Documentation Verification Report

Pretopology

📁 Source: Mathlib/CategoryTheory/Sites/Pretopology.lean

Statistics

Metric	Count
Definitions `toPretopology`, `toPretopology`, `Pretopology`, `LE`, `gi`, `instCoeFunForallSetPresieve`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instPartialOrder`, `ofGrothendieck`, `orderBot`, `orderTop`, `toGrothendieck`, `toPrecoverage`, `trivial`	16
Theorems `mem_toPretopology`, `toPretopology_toPrecoverage`, `ext`, `ext_iff`, `has_isos`, `isGLB_sInf`, `le_def`, `mem_inf`, `mem_ofGrothendieck`, `mem_sInf`, `mem_toGrothendieck`, `pullbacks`, `sInf_ofGrothendieck`, `toGrothendieck_bot`, `toGrothendieck_mono`, `transitive`	16
Total	32

CategoryTheory

Definitions

Name	Category	Theorems
`Pretopology` 📖	CompData	14 math math: `AlgebraicGeometry.Scheme.pretopology_le_pretopology`, `MorphismProperty.pretopology_monotone`, `AlgebraicGeometry.Scheme.pretopology_le_inf`, `AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf`, `MorphismProperty.pretopology_inf`, `Pretopology.mem_inf`, `Pretopology.isGLB_sInf`, `Pretopology.mem_sInf`, `Pretopology.toGrothendieck_bot`, `AlgebraicGeometry.Scheme.pretopology_monotone`, `Pretopology.le_def`, `AlgebraicGeometry.Scheme.pretopology_eq_inf`, `MorphismProperty.pretopology_le`, `Pretopology.sInf_ofGrothendieck`

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`toPretopology` 📖	CompOp	5 math math: `mem_toPretopology`, `Opens.pretopology_ofGrothendieck`, `Opens.toPretopology_grothendieckTopology`, `CategoryTheory.Pretopology.mem_ofGrothendieck`, `CategoryTheory.Pretopology.sInf_ofGrothendieck`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_toPretopology` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Pretopology.toPrecoverage` `toPretopology` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Sieve.generate`	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
`toPretopology` 📖	CompOp	2 math math: `toGrothendieck_toPretopology_eq_toGrothendieck`, `toPretopology_toPrecoverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPretopology_toPrecoverage` 📖	mathematical	—	`CategoryTheory.Pretopology.toPrecoverage` `toPretopology`	—	—

CategoryTheory.Pretopology

Definitions

Name	Category	Theorems
`LE` 📖	CompOp	7 math math: `AlgebraicGeometry.Scheme.pretopology_le_pretopology`, `CategoryTheory.MorphismProperty.pretopology_monotone`, `isGLB_sInf`, `toGrothendieck_bot`, `AlgebraicGeometry.Scheme.pretopology_monotone`, `le_def`, `CategoryTheory.MorphismProperty.pretopology_le`
`gi` 📖	CompOp	—
`instCoeFunForallSetPresieve` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	5 math math: `AlgebraicGeometry.Scheme.pretopology_le_inf`, `AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf`, `CategoryTheory.MorphismProperty.pretopology_inf`, `mem_inf`, `AlgebraicGeometry.Scheme.pretopology_eq_inf`
`instInfSet` 📖	CompOp	3 math math: `isGLB_sInf`, `mem_sInf`, `sInf_ofGrothendieck`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`ofGrothendieck` 📖	CompOp	—
`orderBot` 📖	CompOp	1 math math: `toGrothendieck_bot`
`orderTop` 📖	CompOp	—
`toGrothendieck` 📖	CompOp	16 math math: `AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology`, `AlgebraicGeometry.Scheme.zariskiTopology_eq`, `Opens.pretopology_toGrothendieck`, `CategoryTheory.Presieve.isSheaf_pretopology`, `toGrothendieck_mono`, `mem_toGrothendieck`, `AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf`, `AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology`, `CategoryTheory.MorphismProperty.grothendieckTopology_eq_toGrothendieck_pretopology`, `toGrothendieck_toCoverage`, `AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology`, `AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`, `toGrothendieck_bot`, `CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck`, `AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology`, `CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology`
`toPrecoverage` 📖	CompOp	17 math math: `CategoryTheory.GrothendieckTopology.mem_toPretopology`, `AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology`, `mem_toGrothendieck`, `ext_iff`, `CategoryTheory.MorphismProperty.pretopology_toPrecoverage`, `has_isos`, `mem_inf`, `ofArrows_mem_finite`, `mem_sInf`, `CategoryTheory.Precoverage.toPretopology_toPrecoverage`, `mem_toCoverage`, `AlgebraicGeometry.Scheme.mem_pretopology_iff`, `AlgebraicGeometry.Scheme.Cover.mem_pretopology`, `mem_ofGrothendieck`, `le_def`, `AlgebraicGeometry.Scheme.pretopology_cover`, `finite_toPrecoverage`
`trivial` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.Precoverage.coverings` `toPrecoverage`	—	—	`CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks`
`ext_iff` 📖	mathematical	—	`CategoryTheory.Precoverage.coverings` `toPrecoverage`	—	`ext`
`has_isos` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Presieve.singleton`	—	—
`isGLB_sInf` 📖	mathematical	—	`IsGLB` `CategoryTheory.Pretopology` `LE` `InfSet.sInf` `instInfSet`	—	`IsGLB.of_image` `isGLB_sInf`
`le_def` 📖	mathematical	—	`CategoryTheory.Pretopology` `LE` `Pi.hasLe` `Set` `CategoryTheory.Presieve` `Set.instLE` `CategoryTheory.Precoverage.coverings` `toPrecoverage`	—	—
`mem_inf` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Pretopology` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	—
`mem_ofGrothendieck` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.GrothendieckTopology.toPretopology` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.generate`	—	`CategoryTheory.GrothendieckTopology.mem_toPretopology`
`mem_sInf` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `InfSet.sInf` `CategoryTheory.Pretopology` `instInfSet`	—	`Set.iInter_coe_set` `Set.iInter_congr_Prop` `Set.iInter_exists` `Set.biInter_and'` `Set.iInter_iInter_eq_right`
`mem_toGrothendieck` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `toGrothendieck` `CategoryTheory.Presieve` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve` `CategoryTheory.Sieve.arrows`	—	—
`pullbacks` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage`	`CategoryTheory.Presieve.pullbackArrows` `CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks`	—	—
`sInf_ofGrothendieck` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.toPretopology` `InfSet.sInf` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instInfSet` `CategoryTheory.Pretopology` `instInfSet` `Set.image`	—	`ext` `Set.ext`
`toGrothendieck_bot` 📖	mathematical	—	`toGrothendieck` `Bot.bot` `CategoryTheory.Pretopology` `OrderBot.toBot` `LE` `orderBot` `CategoryTheory.GrothendieckTopology` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.GrothendieckTopology.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`toGrothendieck_mono` 📖	mathematical	`CategoryTheory.Pretopology` `LE`	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `toGrothendieck`	—	—
`transitive` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage`	`CategoryTheory.Presieve.bind`	—	—

---

← Back to Index