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 :
    RingHom.StableUnderComposition fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.respectsIso :
    RingHom.RespectsIso fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.isStableUnderBaseChange :
    RingHom.IsStableUnderBaseChange fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.holdsForLocalizationAway :
    RingHom.HoldsForLocalizationAway fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.ofLocalizationPrime :
    RingHom.OfLocalizationPrime fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.ofLocalizationSpanTarget :
    RingHom.OfLocalizationSpanTarget fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    theorem RingHom.FormallyUnramified.propertyIsLocal :
    RingHom.PropertyIsLocal fun {R S : Type u_3} [CommRing R] [CommRing S] => RingHom.FormallyUnramified