Equalizer of inclusions to pushouts in CommRingCat

Given a map f : R ⟶ S in CommRingCat, we prove that the equalizer of the two maps pushout.inl : S ⟶ pushout f f and pushout.inr : S ⟶ pushout f f is canonically isomorphic to R when R ⟶ S is a faithfully flat ring map.

Note that, under CommRingCat.pushoutCoconeIsColimit, the two maps inl and inr above can be described as s ↦ s ⊗ₜ[R] 1 and s ↦ 1 ⊗ₜ[R] s, respectively.

noncomputable def CommRingCat.isLimitForkPushoutSelfOfFaithfullyFlat {R S : CommRingCat} (f : R ⟶ S) (hf : (Hom.hom f).FaithfullyFlat) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)

If f : R ⟶ S is a faithfully flat map in CommRingCat, then the fork

        S ---inl---> pushout f f
R --f-->
        S ---inr---> pushout f f

is an equalizer diagram.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommRingCat.regularMonoOfFaithfullyFlat {R S : CommRingCat} (f : R ⟶ S) (hf : (Hom.hom f).FaithfullyFlat) : CategoryTheory.RegularMono f

A regular monomorphism structure on a map f : R ⟶ S in CommRingCat with faithfully flat f.hom : R ⟶ S.

Equations

• One or more equations did not get rendered due to their size.

theorem CommRingCat.isRegularMono_of_faithfullyFlat {R S : CommRingCat} (f : R ⟶ S) (hf : (Hom.hom f).FaithfullyFlat) : CategoryTheory.IsRegularMono f

Any map f : R ⟶ S in CommRingCat with faithfully flat f.hom : R ⟶ S is a regular monomorphism.

theorem CommRingCat.Opposite.regularEpiOfFaithfullyFlat {R S : CommRingCatᵒᵖ} (f : S ⟶ R) (hf : (Hom.hom f.unop).FaithfullyFlat) : CategoryTheory.IsRegularEpi f

A regular epimorphism structure on a map f : S ⟶ R in CommRingCatᵒᵖ with faithfully flat f.unop.hom : R.unop ⟶ S.unop.

theorem CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat {R S : CommRingCatᵒᵖ} (f : S ⟶ R) (hf : (Hom.hom f.unop).FaithfullyFlat) : CategoryTheory.EffectiveEpi f

Any map f : S ⟶ R in CommRingCatᵒᵖ with faithfully flat f.unop.hom : R.unop ⟶ S.unop is an effective epimorphism.