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.IsStableUnderBaseChange: 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 : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

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

theorem RingHom.RespectsIso.cancel_left_isIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RespectsIso P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso f] : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) ↔ P (CommRingCat.Hom.hom g)

theorem RingHom.RespectsIso.cancel_right_isIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RespectsIso P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso g] : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) ↔ P (CommRingCat.Hom.hom f)

theorem RingHom.RespectsIso.isLocalization_away_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RespectsIso P) {R S : Type u} (R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] : P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)

theorem RingHom.RespectsIso.and {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hQ : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => Q) : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ Q f

def RingHom.StableUnderComposition (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

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

theorem RingHom.StableUnderComposition.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : StableUnderComposition P) (hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom) : RespectsIso P

theorem RingHom.StableUnderComposition.and {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => P) (hQ : StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => Q) : StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ Q f

def RingHom.IsStableUnderBaseChange (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

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

theorem RingHom.IsStableUnderBaseChange.mk {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (h₁ : RespectsIso P) (h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P (algebraMap S (TensorProduct R S T))) : IsStableUnderBaseChange P

theorem RingHom.IsStableUnderBaseChange.tensorProduct {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) {R S : Type u} (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (h : P (algebraMap R S)) : P (algebraMap T (TensorProduct R T S))

theorem RingHom.IsStableUnderBaseChange.pushout_inl {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : IsStableUnderBaseChange P) (hP' : RespectsIso P) {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T) (H : P (CommRingCat.Hom.hom g)) : P (CommRingCat.Hom.hom (CategoryTheory.Limits.pushout.inl f g))

theorem RingHom.IsStableUnderBaseChange.and {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) (hQ : IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => Q) : IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ Q f

def RingHom.toMorphismProperty (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : CategoryTheory.MorphismProperty CommRingCat

The categorical MorphismProperty associated to a property of ring homs expressed non-categorical terms.

theorem RingHom.toMorphismProperty_respectsIso_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} : (RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) ↔ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P).RespectsIso

theorem RingHom.isStableUnderCobaseChange_toMorphismProperty_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange ↔ IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P

theorem RingHom.RespectsIso.arrow_mk_iso_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQ : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {A B A' B' : CommRingCat} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Variant of MorphismProperty.arrow_mk_iso_iff specialized to morphism properties in CommRingCat given by ring hom properties.

def RingHom.CodescendsAlong (P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

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.

theorem RingHom.CodescendsAlong.mk {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (h₁ : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (TensorProduct R S T)) → P (algebraMap R T)) : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P) fun {R S : Type u} [CommRing R] [CommRing S] => Q

theorem RingHom.CodescendsAlong.algebraMap_tensorProduct {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (R S T : Type u) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hPQ : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P) fun {R S : Type u} [CommRing R] [CommRing S] => Q) (h : Q (algebraMap R S)) (H : P (algebraMap S (TensorProduct R S T))) : P (algebraMap R T)

theorem RingHom.CodescendsAlong.includeRight {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (R S T : Type u) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hPQ : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P) fun {R S : Type u} [CommRing R] [CommRing S] => Q) (h : Q (algebraMap R T)) (H : P Algebra.TensorProduct.includeRight.toRingHom) : P (algebraMap R S)

theorem RingHom.CodescendsAlong.and {P Q P' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P) fun {R S : Type u} [CommRing R] [CommRing S] => Q) (hP' : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => P') fun {R S : Type u} [CommRing R] [CommRing S] => Q) : CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ P' f) fun {R S : Type u} [CommRing R] [CommRing S] => Q

def RingHom.HasEqualizers (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

A property of ring homomorphisms P is said to have equalizers, if the equalizer of algebra maps between algebras satisfying P also satisfies P.

theorem RingHom.HasEqualizers.and {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => P) (hQ : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] => Q) : HasEqualizers fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ Q f

def RingHom.HasFiniteProducts (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : Prop

A property of ring homomorphisms P is said to have finite products, if a finite product of algebras satisfying Q also satisfies P.

theorem RingHom.HasFiniteProducts.and {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => P) (hQ : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] => Q) : HasFiniteProducts fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) => P f ∧ Q f