ZeroFamily

📁 Source: Mathlib/CategoryTheory/Sites/Hypercover/ZeroFamily.lean

Statistics

Metric	Count
Definitions PreZeroHypercoverFamily, precoverage, presieve, property, equivPreZeroHypercoverFamily, preZeroHypercoverFamily, instCoeFunPreZeroHypercoverFamilyForallForallPreZeroHypercoverProp	7
Theorems presieve₀_mem_precoverage_iff, ext, ext_iff, iff_shrink, mem_precoverage_iff, of_preZeroHypercoverFamily, of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms, of_preZeroHypercoverFamily, of_preZeroHypercoverFamily, preZeroHypercoverFamily_property	10
Total	17

CategoryTheory

Definitions

Name	Category	Theorems
PreZeroHypercoverFamily 📖	CompData	—
instCoeFunPreZeroHypercoverFamilyForallForallPreZeroHypercoverProp 📖	CompOp	—

CategoryTheory.PreZeroHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presieve₀_mem_precoverage_iff 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercoverFamily.precoverage presieve₀ CategoryTheory.PreZeroHypercoverFamily.property	—	CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff CategoryTheory.PreZeroHypercoverFamily.iff_shrink shrink_eq_shrink_of_presieve₀_eq_presieve₀

CategoryTheory.PreZeroHypercoverFamily

Definitions

Name	Category	Theorems
precoverage 📖	CompOp	6 math math: CategoryTheory.Precoverage.IsStableUnderSup.of_preZeroHypercoverFamily, CategoryTheory.Precoverage.HasIsos.of_preZeroHypercoverFamily, mem_precoverage_iff, CategoryTheory.Precoverage.IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms, CategoryTheory.Precoverage.IsStableUnderComposition.of_preZeroHypercoverFamily, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff
presieve 📖	CompData	—
property 📖	CompOp	6 math math: ext_iff, CategoryTheory.Precoverage.preZeroHypercoverFamily_property, iff_shrink, mem_precoverage_iff, AlgebraicGeometry.Scheme.qcCoverFamily_property, CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	property	—	—	—
ext_iff 📖	mathematical	—	property	—	ext
iff_shrink 📖	mathematical	—	property CategoryTheory.PreZeroHypercover.shrink	—	—
mem_precoverage_iff 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings precoverage property CategoryTheory.PreZeroHypercover.presieve₀	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
equivPreZeroHypercoverFamily 📖	CompOp	—
preZeroHypercoverFamily 📖	CompOp	1 math math: preZeroHypercoverFamily_property

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preZeroHypercoverFamily_property 📖	mathematical	—	CategoryTheory.PreZeroHypercoverFamily.property preZeroHypercoverFamily CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.PreZeroHypercover.presieve₀	—	—

CategoryTheory.Precoverage.HasIsos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_preZeroHypercoverFamily 📖	mathematical	CategoryTheory.PreZeroHypercoverFamily.property CategoryTheory.PreZeroHypercover.singleton	CategoryTheory.Precoverage.HasIsos CategoryTheory.PreZeroHypercoverFamily.precoverage	—	CategoryTheory.PreZeroHypercover.presieve₀_singleton

CategoryTheory.Precoverage.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory CategoryTheory.PreZeroHypercoverFamily.property CategoryTheory.PreZeroHypercover.pullback₁	CategoryTheory.Precoverage.IsStableUnderBaseChange CategoryTheory.PreZeroHypercoverFamily.precoverage	—	CategoryTheory.IsPullback.hasPullback CategoryTheory.IsPullback.isoPullback_hom_fst CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff CategoryTheory.ObjectProperty.prop_iff_of_iso

CategoryTheory.Precoverage.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_preZeroHypercoverFamily 📖	mathematical	CategoryTheory.PreZeroHypercoverFamily.property CategoryTheory.PreZeroHypercover.bind	CategoryTheory.Precoverage.IsStableUnderComposition CategoryTheory.PreZeroHypercoverFamily.precoverage	—	CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff

CategoryTheory.Precoverage.IsStableUnderSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_preZeroHypercoverFamily 📖	mathematical	CategoryTheory.PreZeroHypercoverFamily.property CategoryTheory.PreZeroHypercover.sum	CategoryTheory.Precoverage.IsStableUnderSup CategoryTheory.PreZeroHypercoverFamily.precoverage	—	CategoryTheory.Presieve.exists_eq_preZeroHypercover CategoryTheory.PreZeroHypercover.presieve₀_sum CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff

---

← Back to Index