Properties of ring homomorphisms #
We provide the basic framework for talking about properties of ring homomorphisms. The following meta-properties of predicates on ring homomorphisms are defined
RingHom.RespectsIso
:P
respects isomorphisms ifP f → P (e ≫ f)
andP f → P (f ≫ e)
, wheree
is an isomorphism.RingHom.StableUnderComposition
:P
is stable under composition ifP f → P g → P (f ≫ g)
.RingHom.IsStableUnderBaseChange
:P
is stable under base change ifP (S ⟶ Y)
impliesP (X ⟶ X ⊗[S] Y)
.
A property RespectsIso
if it still holds when composed with an isomorphism
Equations
- One or more equations did not get rendered due to their size.
Instances For
A property is StableUnderComposition
if the composition of two such morphisms
still falls in the class.
Equations
Instances For
A morphism property P
is IsStableUnderBaseChange
if P(S →+* A)
implies
P(B →+* A ⊗[S] B)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The categorical MorphismProperty
associated to a property of ring homs expressed
non-categorical terms.
Equations
- RingHom.toMorphismProperty P f = P (CommRingCat.Hom.hom f)
Instances For
Variant of MorphismProperty.arrow_mk_iso_iff
specialized to morphism properties in
CommRingCat
given by ring hom properties.
A property of ring homomorphisms Q
codescends along Q'
if whenever
R' →+* R' ⊗[R] S
satisfies Q
and R →+* R'
satisfies Q'
, then R →+* S
satisfies Q
.
Equations
- One or more equations did not get rendered due to their size.