Documentation

Mathlib.RingTheory.RingHom.Etale

É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) :

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

Instances For

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) :

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

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