mathlib3 documentation

ring_theory.ring_hom_properties

Properties of ring homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We provide the basic framework for talking about properties of ring homomorphisms. The following meta-properties of predicates on ring homomorphisms are defined

def ring_hom.respects_iso (P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (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 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) Prop} (hP : ring_hom.respects_iso P) {R S T : CommRing} (f : R S) (g : S T) [category_theory.is_iso f] :
P (f g) P g
theorem ring_hom.respects_iso.cancel_right_is_iso {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) Prop} (hP : ring_hom.respects_iso P) {R S T : CommRing} (f : R S) (g : S T) [category_theory.is_iso g] :
P (f g) P f
theorem ring_hom.respects_iso.is_localization_away_iff {P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (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'] [algebra R R'] [algebra S S'] (f : R →+* S) (r : R) [is_localization.away r R'] [is_localization.away (f r) S'] :
def ring_hom.stable_under_composition (P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (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 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) Prop} (hP : ring_hom.stable_under_composition P) (hP' : {R S : Type u} [_inst_3 : comm_ring R] [_inst_4 : comm_ring S] (e : R ≃+* S), P e.to_ring_hom) :
def ring_hom.stable_under_base_change (P : Π {R S : Type u} [_inst_1 : comm_ring R] [_inst_2 : comm_ring S], (R →+* S) Prop) :
Prop

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

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