Documentation

Mathlib.RingTheory.RingHom.Unramified

The meta properties of unramified ring homomorphisms. #

source
def RingHom.FormallyUnramified {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring homomorphism R →+* A is formally unramified if Ω[A⁄R] is trivial. See Algebra.FormallyUnramified.

Equations
Instances For
    source
    theorem RingHom.formallyUnramified_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S
    source
    theorem RingHom.FormallyUnramified.of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) :
    f.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.of_comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} (h : (g.comp f).FormallyUnramified) :
    g.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.FormallyUnramified) (hg : g.FormallyUnramified) :
    (g.comp f).FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.stableUnderComposition :
    StableUnderComposition fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.respectsIso :
    RespectsIso fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.isStableUnderBaseChange :
    IsStableUnderBaseChange fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.holdsForLocalization :
    HoldsForLocalization fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.holdsForLocalizationAway :
    HoldsForLocalizationAway fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.ofLocalizationPrime :
    OfLocalizationPrime fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.ofLocalizationSpanTarget :
    OfLocalizationSpanTarget fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.propertyIsLocal :
    PropertyIsLocal fun {R S : Type u_3} [CommRing R] [CommRing S] => FormallyUnramified
    source
    theorem RingHom.FormallyEtale.of_comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {T : Type u_3} [CommRing T] {f : R →+* S} {g : S →+* T} (hf : f.FormallyUnramified) (h : (g.comp f).FormallyEtale) :
    g.FormallyEtale