Comparison

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean

Statistics

Metric	Count
Definitions	0
Theorems extensive_regular_generate_coherent, instPrecoherentOfFinitaryPreExtensiveOfPreregular, instPreregularOfPrecoherentOfHasFiniteCoproducts	3
Total	3

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extensive_regular_generate_coherent 📖	mathematical	—	Coverage.toGrothendieck Coverage SemilatticeSup.toMax Coverage.instSemilatticeSup extensiveCoverage regularCoverage coherentTopology instPrecoherentOfFinitaryPreExtensiveOfPreregular	—	GrothendieckTopology.ext instPrecoherentOfFinitaryPreExtensiveOfPreregular Set.ext instEffectiveEpiFamilyOfIsIsoDesc Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Finite.of_fintype instEffectiveEpiFamily instEffectiveEpiDescOfEffectiveEpiFamily Sieve.pullback_comp GrothendieckTopology.pullback_stable Limits.colimit.ι_desc Category.assoc Coverage.saturate_of_superset Limits.Sigma.hom_ext Category.comp_id IsIso.id
instPrecoherentOfFinitaryPreExtensiveOfPreregular 📖	mathematical	—	Precoherent	—	Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Preregular.exists_fac instEffectiveEpiDescOfEffectiveEpiFamily FinitaryPreExtensive.hasPullbacks_of_inclusions Limits.instIsIsoDescι FinitaryPreExtensive.isIso_sigmaDesc_fst Limits.Sigma.hom_ext Limits.colimit.ι_desc_assoc Limits.colimit.ι_desc effectiveEpi_desc_iff_effectiveEpiFamily instEffectiveEpiOfEffectiveEpiFamily instEffectiveEpiFamilyCompOfIsSplitEpi IsSplitEpi.of_iso instEffectiveEpiFamily Category.assoc Limits.pullback.condition
instPreregularOfPrecoherentOfHasFiniteCoproducts 📖	mathematical	—	Preregular	—	Precoherent.pullback Finite.of_fintype effectiveEpi_iff_effectiveEpiFamily Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete instEffectiveEpiDescOfEffectiveEpiFamily Limits.Sigma.hom_ext Limits.colimit.ι_desc_assoc

---

← Back to Index