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 : 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 : RingHom.RespectsIso P) {R : CommRingCat} {S : CommRingCat} {T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso f] : P (↑R) (↑T) (CommRingCat.instCommRingα R) (CommRingCat.instCommRingα T) (CategoryTheory.CategoryStruct.comp f g) ↔ P (↑S) (↑T) (CommRingCat.instCommRingα S) (CommRingCat.instCommRingα T) g

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

theorem RingHom.RespectsIso.is_localization_away_iff {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {R : Type u} {S : Type u} (R' : Type u) (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.Away r) (Localization.Away (↑f r)) Localization.instCommRingLocalizationToCommMonoid Localization.instCommRingLocalizationToCommMonoid (Localization.awayMap f r) ↔ P R' S' inst✝ inst✝¹ (IsLocalization.Away.map R' S' f r)

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 : RingHom.StableUnderComposition P) (hP' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (e : R ≃+* S) → P R S inst inst_1 (RingEquiv.toRingHom e)) : RingHom.RespectsIso P

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

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

theorem RingHom.StableUnderBaseChange.mk (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (h₁ : RingHom.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 R T inst inst_2 (algebraMap R T) → P S (TensorProduct R S T) inst_1 Algebra.TensorProduct.instCommRing Algebra.TensorProduct.includeLeftRingHom) : RingHom.StableUnderBaseChange P

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