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