mathlibdocumentation

ring_theory.ring_hom_properties

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

• ring_hom.respects_iso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.
• ring_hom.stable_under_composition: P is stable under composition if P f → P g → P (f ≫ g).
• ring_hom.stable_under_base_change: P is stable under base change if P (S ⟶ Y) implies P (X ⟶ X ⊗[S] Y).
def ring_hom.respects_iso (P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop) :
Prop

A property respects_iso if it still holds when composed with an isomorphism

Equations
theorem ring_hom.respects_iso.cancel_left_is_iso {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {R S T : CommRing} (f : R S) (g : S T)  :
P (f g) P g
theorem ring_hom.respects_iso.cancel_right_is_iso {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {R S T : CommRing} (f : R S) (g : S T)  :
P (f g) P f
theorem ring_hom.respects_iso.is_localization_away_iff {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP : ring_hom.respects_iso P) {R S : Type u} (R' S' : Type u) [comm_ring R] [comm_ring S] [comm_ring R'] [comm_ring S'] [ R'] [ S'] (f : R →+* S) (r : R) [ R'] [ S'] :
P P S' f r)
def ring_hom.stable_under_composition (P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop) :
Prop

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

Equations
theorem ring_hom.stable_under_composition.respects_iso {P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop} (hP' : {R S : Type u} [_inst_3 : [_inst_4 : (e : R ≃+* S), P e.to_ring_hom) :
def ring_hom.stable_under_base_change (P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop) :
Prop

A morphism property P is stable_under_base_change if P(S →+* A) implies P(B →+* A ⊗[S] B).

Equations
• = (R S R' S' : Type u) [_inst_3 : [_inst_4 : [_inst_5 : comm_ring R'] [_inst_6 : comm_ring S'] [_inst_7 : S] [_inst_8 : R'] [_inst_9 : S'] [_inst_10 : S'] [_inst_11 : algebra R' S'] [_inst_7_1 : S'] [_inst_8_1 : R' S'] [_inst_7_1 : R' S'], P S) P (algebra_map R' S')
theorem ring_hom.stable_under_base_change.mk (P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop) (h₁ : ring_hom.respects_iso P) (h₂ : ⦃R S T : Type u⦄ [_inst_3 : [_inst_4 : [_inst_5 : [_inst_6 : S] [_inst_7 : T], ) :
theorem ring_hom.stable_under_base_change.pushout_inl (P : Π {R S : Type u} [_inst_1 : [_inst_2 : , (R →+* S) Prop) (hP' : ring_hom.respects_iso P) {R S T : CommRing} (f : R S) (g : R T) (H : P g) :