Documentation

Mathlib.RingTheory.RingHom.Etale

Étale ring homomorphisms #

We show the meta properties of étale morphisms.

source
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.

Equations
Instances For
    source
    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

    source
    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
    source
    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
    source
    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
    source
    theorem RingHom.Etale.formallyUnramified {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.Etale) :
    f.FormallyUnramified
    source
    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
    source
    theorem RingHom.Etale.containsIdentities :
    ContainsIdentities fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.isStableUnderBaseChange :
    IsStableUnderBaseChange fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.propertyIsLocal :
    PropertyIsLocal fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.respectsIso :
    RespectsIso fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.ofLocalizationSpanTarget :
    OfLocalizationSpanTarget fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.ofLocalizationSpan :
    OfLocalizationSpan fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.stableUnderComposition :
    StableUnderComposition fun {R S : Type u_5} [CommRing R] [CommRing S] => Etale
    source
    theorem RingHom.Etale.iff_flat_and_formallyUnramified {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} :
    f.Etale ↔ f.Flat ∧ f.FormallyUnramified ∧ f.FinitePresentation