Etale ring homomorphisms

We show the meta properties of étale morphisms.

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

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

Equations

• f.Etale = Algebra.Etale R S

theorem RingHom.Etale.toAlgebra {R S : Type u} [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 S : Type u} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).Etale ↔ Algebra.Etale R S

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

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

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

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

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

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

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

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