Étale ring homomorphisms

We show the meta properties of étale morphisms.

def RingHom.Etale {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A ring hom R →+* S is étale, if S is an étale R-algebra.

theorem RingHom.Etale.toAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Etale) : Algebra.Etale R S

Helper lemma for the algebraize tactic

theorem RingHom.etale_algebraMap {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).Etale ↔ Algebra.Etale R S

theorem RingHom.etale_iff_formallyUnramified_and_smooth {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) : f.Etale ↔ f.FormallyUnramified ∧ f.Smooth

theorem RingHom.Etale.eq_formallyUnramified_and_smooth : @Etale = fun (R : Type u_6) (S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) => f.FormallyUnramified ∧ f.Smooth

theorem RingHom.Etale.formallyUnramified {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.Etale) : f.FormallyUnramified

theorem RingHom.Etale.of_bijective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) : f.Etale

theorem RingHom.Etale.containsIdentities : ContainsIdentities fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.isStableUnderBaseChange : IsStableUnderBaseChange fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.propertyIsLocal : PropertyIsLocal fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.respectsIso : RespectsIso fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.ofLocalizationSpanTarget : OfLocalizationSpanTarget fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.ofLocalizationSpan : OfLocalizationSpan fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale

theorem RingHom.Etale.stableUnderComposition : StableUnderComposition fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale