Documentation Verification Report

Saturate

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

Statistics

Metric	Count
Definitions `Saturate`, `fst`, `obj`, `snd`, `fromSaturateOfHasPullbacks`, `fromSaturateToSaturateHomotopy`, `isLimitSaturateEquivOfHasPullbacks`, `saturate`, `sectionsSaturateEquiv`, `toPreOneHypercoverHomotopy`, `toSaturateOfHasPullbacks`, `Saturate`	12
Theorems `w`, `fromSaturateOfHasPullbacks_h₀`, `fromSaturateOfHasPullbacks_h₁`, `fromSaturateOfHasPullbacks_s₀`, `fromSaturateOfHasPullbacks_s₁`, `isLimit_saturate_type_iff`, `saturate_I₁`, `saturate_Y`, `saturate_p₁`, `saturate_p₂`, `saturate_toPreZeroHypercover`, `sectionsSaturateEquiv_apply_coe`, `sectionsSaturateEquiv_symm_apply_val`, `toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks`, `toSaturateOfHasPullbacks_h₀`, `toSaturateOfHasPullbacks_h₁`, `toSaturateOfHasPullbacks_s₀`, `toSaturateOfHasPullbacks_s₁_fst`, `toSaturateOfHasPullbacks_s₁_obj`, `toSaturateOfHasPullbacks_s₁_snd`	20
Total	32

CategoryTheory.Coverage

Definitions

Name	Category	Theorems
`Saturate` 📖	CompData	4 math math: `saturate_iff_saturate_toPrecoverage`, `Saturate.pullback`, `saturate_of_superset`, `mem_toGrothendieck`

CategoryTheory.PreZeroHypercover

Definitions

Name	Category	Theorems
`fromSaturateOfHasPullbacks` 📖	CompOp	5 math math: `toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks`, `fromSaturateOfHasPullbacks_s₁`, `fromSaturateOfHasPullbacks_s₀`, `fromSaturateOfHasPullbacks_h₀`, `fromSaturateOfHasPullbacks_h₁`
`fromSaturateToSaturateHomotopy` 📖	CompOp	—
`isLimitSaturateEquivOfHasPullbacks` 📖	CompOp	—
`saturate` 📖	CompOp	19 math math: `saturate_I₁`, `toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks`, `toSaturateOfHasPullbacks_h₀`, `fromSaturateOfHasPullbacks_s₁`, `toSaturateOfHasPullbacks_s₀`, `toSaturateOfHasPullbacks_h₁`, `sectionsSaturateEquiv_apply_coe`, `saturate_p₁`, `toSaturateOfHasPullbacks_s₁_snd`, `toSaturateOfHasPullbacks_s₁_obj`, `saturate_p₂`, `toSaturateOfHasPullbacks_s₁_fst`, `saturate_toPreZeroHypercover`, `sectionsSaturateEquiv_symm_apply_val`, `fromSaturateOfHasPullbacks_s₀`, `isLimit_saturate_type_iff`, `fromSaturateOfHasPullbacks_h₀`, `saturate_Y`, `fromSaturateOfHasPullbacks_h₁`
`sectionsSaturateEquiv` 📖	CompOp	2 math math: `sectionsSaturateEquiv_apply_coe`, `sectionsSaturateEquiv_symm_apply_val`
`toPreOneHypercoverHomotopy` 📖	CompOp	—
`toSaturateOfHasPullbacks` 📖	CompOp	7 math math: `toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks`, `toSaturateOfHasPullbacks_h₀`, `toSaturateOfHasPullbacks_s₀`, `toSaturateOfHasPullbacks_h₁`, `toSaturateOfHasPullbacks_s₁_snd`, `toSaturateOfHasPullbacks_s₁_obj`, `toSaturateOfHasPullbacks_s₁_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromSaturateOfHasPullbacks_h₀` 📖	mathematical	`HasPullbacks`	`Hom.h₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `saturate` `toPreOneHypercover` `CategoryTheory.PreOneHypercover.Hom.toHom` `fromSaturateOfHasPullbacks` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `X`	—	—
`fromSaturateOfHasPullbacks_h₁` 📖	mathematical	`HasPullbacks`	`CategoryTheory.PreOneHypercover.Hom.h₁` `saturate` `toPreOneHypercover` `fromSaturateOfHasPullbacks` `CategoryTheory.Limits.pullback.lift` `CategoryTheory.PreOneHypercover.Y` `X` `f` `Relation.fst` `Relation.snd` `Relation.w`	—	—
`fromSaturateOfHasPullbacks_s₀` 📖	mathematical	`HasPullbacks`	`Hom.s₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `saturate` `toPreOneHypercover` `CategoryTheory.PreOneHypercover.Hom.toHom` `fromSaturateOfHasPullbacks`	—	—
`fromSaturateOfHasPullbacks_s₁` 📖	mathematical	`HasPullbacks`	`CategoryTheory.PreOneHypercover.Hom.s₁` `saturate` `toPreOneHypercover` `fromSaturateOfHasPullbacks`	—	—
`isLimit_saturate_type_iff` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.PreOneHypercover.multicospanShape` `saturate` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.types` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.PreOneHypercover.multifork` `CategoryTheory.Presieve.IsSheafFor` `presieve₀`	—	`CategoryTheory.Limits.Multifork.isLimit_types_iff` `CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible` `Function.Bijective.of_comp_iff'` `Equiv.bijective`
`saturate_I₁` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.I₁` `saturate` `Relation`	—	—
`saturate_Y` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.Y` `saturate` `Relation.obj`	—	—
`saturate_p₁` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.p₁` `saturate` `Relation.fst`	—	—
`saturate_p₂` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.p₂` `saturate` `Relation.snd`	—	—
`saturate_toPreZeroHypercover` 📖	mathematical	—	`CategoryTheory.PreOneHypercover.toPreZeroHypercover` `saturate`	—	—
`sectionsSaturateEquiv_apply_coe` 📖	mathematical	—	`CategoryTheory.Presieve.Arrows.Compatible` `I₀` `X` `f` `DFunLike.coe` `Equiv` `CategoryTheory.Limits.MulticospanIndex.sections` `CategoryTheory.PreOneHypercover.multicospanShape` `saturate` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.types` `EquivLike.toFunLike` `Equiv.instEquivLike` `sectionsSaturateEquiv` `CategoryTheory.Limits.MulticospanIndex.sections.val`	—	—
`sectionsSaturateEquiv_symm_apply_val` 📖	mathematical	—	`CategoryTheory.Limits.MulticospanIndex.sections.val` `CategoryTheory.PreOneHypercover.multicospanShape` `saturate` `CategoryTheory.PreOneHypercover.multicospanIndex` `CategoryTheory.types` `DFunLike.coe` `Equiv` `CategoryTheory.Presieve.Arrows.Compatible` `I₀` `X` `f` `CategoryTheory.Limits.MulticospanIndex.sections` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sectionsSaturateEquiv`	—	—
`toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks` 📖	mathematical	`HasPullbacks`	`CategoryTheory.PreOneHypercover.Hom.comp` `toPreOneHypercover` `saturate` `toSaturateOfHasPullbacks` `fromSaturateOfHasPullbacks` `CategoryTheory.PreOneHypercover.Hom.id`	—	`CategoryTheory.PreOneHypercover.Hom.ext'` `CategoryTheory.Category.comp_id` `CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl` `CategoryTheory.Limits.pullback.lift_fst_snd` `CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl`
`toSaturateOfHasPullbacks_h₀` 📖	mathematical	`HasPullbacks`	`Hom.h₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `toPreOneHypercover` `saturate` `CategoryTheory.PreOneHypercover.Hom.toHom` `toSaturateOfHasPullbacks` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `X`	—	—
`toSaturateOfHasPullbacks_h₁` 📖	mathematical	`HasPullbacks`	`CategoryTheory.PreOneHypercover.Hom.h₁` `toPreOneHypercover` `saturate` `toSaturateOfHasPullbacks` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreOneHypercover.Y`	—	—
`toSaturateOfHasPullbacks_s₀` 📖	mathematical	`HasPullbacks`	`Hom.s₀` `CategoryTheory.PreOneHypercover.toPreZeroHypercover` `toPreOneHypercover` `saturate` `CategoryTheory.PreOneHypercover.Hom.toHom` `toSaturateOfHasPullbacks`	—	—
`toSaturateOfHasPullbacks_s₁_fst` 📖	mathematical	`HasPullbacks`	`Relation.fst` `CategoryTheory.PreOneHypercover.Hom.s₁` `toPreOneHypercover` `saturate` `toSaturateOfHasPullbacks` `CategoryTheory.Limits.pullback.fst` `X` `f`	—	—
`toSaturateOfHasPullbacks_s₁_obj` 📖	mathematical	`HasPullbacks`	`Relation.obj` `CategoryTheory.PreOneHypercover.Hom.s₁` `toPreOneHypercover` `saturate` `toSaturateOfHasPullbacks` `CategoryTheory.Limits.pullback` `X` `f`	—	—
`toSaturateOfHasPullbacks_s₁_snd` 📖	mathematical	`HasPullbacks`	`Relation.snd` `CategoryTheory.PreOneHypercover.Hom.s₁` `toPreOneHypercover` `saturate` `toSaturateOfHasPullbacks` `CategoryTheory.Limits.pullback.snd` `X` `f`	—	—

CategoryTheory.PreZeroHypercover.Relation

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	4 math math: `CategoryTheory.PreZeroHypercover.saturate_p₁`, `w`, `CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_fst`, `CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁`
`obj` 📖	CompOp	3 math math: `CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_obj`, `w`, `CategoryTheory.PreZeroHypercover.saturate_Y`
`snd` 📖	CompOp	4 math math: `CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_snd`, `CategoryTheory.PreZeroHypercover.saturate_p₂`, `w`, `CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.PreZeroHypercover.X` `fst` `CategoryTheory.PreZeroHypercover.f` `snd`	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
`Saturate` 📖	CompData	2 math math: `CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage`, `mem_toGrothendieck_iff`

---

← Back to Index