EqualizerPushout

📁 Source: Mathlib/Algebra/Category/Ring/EqualizerPushout.lean

Statistics

Metric	Count
Definitions isLimitForkPushoutSelfOfFaithfullyFlat, regularMonoOfFaithfullyFlat	2
Theorems effectiveEpi_of_faithfullyFlat, regularEpiOfFaithfullyFlat, isRegularMono_of_faithfullyFlat	3
Total	5

CommRingCat

Definitions

Name	Category	Theorems
isLimitForkPushoutSelfOfFaithfullyFlat 📖	CompOp	—
regularMonoOfFaithfullyFlat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRegularMono_of_faithfullyFlat 📖	mathematical	—	CategoryTheory.IsRegularMono CommRingCat instCategory	—	CategoryTheory.isRegularMono_of_regularMono

CommRingCat.Opposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpi_of_faithfullyFlat 📖	mathematical	—	CategoryTheory.EffectiveEpi Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory	—	CategoryTheory.isRegularEpi_iff_effectiveEpi CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbacks_opposite CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat regularEpiOfFaithfullyFlat
regularEpiOfFaithfullyFlat 📖	mathematical	—	CategoryTheory.IsRegularEpi Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory	—	CategoryTheory.isRegularEpi_op_iff_isRegularMono CommRingCat.isRegularMono_of_faithfullyFlat

---

← Back to Index