# 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 if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.
• RingHom.StableUnderComposition: P is stable under composition if P f → P g → P (f ≫ g).
• RingHom.StableUnderBaseChange: P is stable under base change if P (S ⟶ Y) implies P (X ⟶ X ⊗[S] Y).
def RingHom.RespectsIso (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

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
theorem RingHom.RespectsIso.cancel_left_isIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : ) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) :
P g
theorem RingHom.RespectsIso.cancel_right_isIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : ) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : S T) :
P f
theorem RingHom.RespectsIso.is_localization_away_iff {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : ) {R : Type u} {S : Type u} (R' : Type u) (S' : Type u) [] [] [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (f : R →+* S) (r : R) [] [IsLocalization.Away (f r) S'] :
P () P (IsLocalization.Away.map R' S' f r)
def RingHom.StableUnderComposition (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

A property is StableUnderComposition if the composition of two such morphisms still falls in the class.

Equations
• = ∀ ⦃R S T : Type u⦄ [inst : ] [inst_1 : ] [inst_2 : ] (f : R →+* S) (g : S →+* T), P fP gP (g.comp f)
Instances For
theorem RingHom.StableUnderComposition.respectsIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop} (hP : ) (hP' : ∀ {R S : Type u} [inst : ] [inst_1 : ] (e : R ≃+* S), P e.toRingHom) :
def RingHom.StableUnderBaseChange (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) :

A morphism property P is StableUnderBaseChange 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
theorem RingHom.StableUnderBaseChange.mk (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (h₁ : ) (h₂ : ∀ ⦃R S T : Type u⦄ [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P ()P Algebra.TensorProduct.includeLeftRingHom) :
theorem RingHom.StableUnderBaseChange.pushout_inl (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S)Prop) (hP : ) (hP' : ) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R S) (g : R T) (H : P g) :
P CategoryTheory.Limits.pushout.inl