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

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).

source

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

ring_hom.respects_iso P = ((∀ {R S T : Type u} [_inst_3 : comm_ring R] [_inst_4 : comm_ring S] [_inst_5 : comm_ring T] (f : R →+* S) (e : S ≃+* T), P f → P (e.to_ring_hom.comp f)) ∧ ∀ {R S T : Type u} [_inst_6 : comm_ring R] [_inst_7 : comm_ring S] [_inst_8 : comm_ring T] (f : S →+* T) (e : R ≃+* S), P f → P (f.comp e.to_ring_hom))

source

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

source

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

source

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'] :

P (localization.away_map f r) ↔ P (is_localization.away.map R' S' f r)

source

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

ring_hom.stable_under_composition P = ∀ ⦃R S T : Type u⦄ [_inst_3 : comm_ring R] [_inst_4 : comm_ring S] [_inst_5 : comm_ring T] (f : R →+* S) (g : S →+* T), P f → P g → P (g.comp f)

source

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) :

ring_hom.respects_iso P

source

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

ring_hom.stable_under_base_change P = ∀ (R S R' S' : Type u) [_inst_3 : comm_ring R] [_inst_4 : comm_ring S] [_inst_5 : comm_ring R'] [_inst_6 : comm_ring S'] [_inst_7 : algebra R S] [_inst_8 : algebra R R'] [_inst_9 : algebra R S'] [_inst_10 : algebra S S'] [_inst_11 : algebra R' S'] [_inst_7_1 : is_scalar_tower R S S'] [_inst_8_1 : is_scalar_tower R R' S'] [_inst_7_1 : algebra.is_pushout R S R' S'], P (algebra_map R S) → P (algebra_map R' S')

source

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) :

ring_hom.stable_under_base_change P

source

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) :

P category_theory.limits.pushout.inl