Pretopology

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

Statistics

Metric	Count
Definitions grothendieckTopology, jointlySurjectivePretopology, jointlySurjectiveTopology, pretopology, surjectiveFamiliesPretopology	5
Theorems mem_grothendieckTopology, mem_pretopology, bot_mem_grothendieckTopology, exists_cover_of_mem_grothendieckTopology, exists_cover_of_mem_pretopology, grothendieckTopology_cover, grothendieckTopology_eq_inf, grothendieckTopology_le_grothendieckTopology, grothendieckTopology_monotone, instIsStableUnderBaseChangeJointlySurjectivePrecoverage, jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology, mem_grothendieckTopology_iff, mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, mem_pretopology_iff, pretopology_cover, pretopology_eq_inf, pretopology_le_inf, pretopology_le_pretopology, pretopology_monotone	19
Total	24

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
grothendieckTopology 📖	CompOp	7 math math: bot_mem_grothendieckTopology, mem_grothendieckTopology_iff, grothendieckTopology_le_grothendieckTopology, grothendieckTopology_eq_inf, grothendieckTopology_monotone, grothendieckTopology_cover, Cover.mem_grothendieckTopology
jointlySurjectivePretopology 📖	CompOp	5 math math: mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, pretopology_le_inf, grothendieckTopology_eq_inf, jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology, pretopology_eq_inf
jointlySurjectiveTopology 📖	CompOp	2 math math: mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology
pretopology 📖	CompOp	7 math math: pretopology_le_pretopology, pretopology_le_inf, pretopology_monotone, mem_pretopology_iff, Cover.mem_pretopology, pretopology_eq_inf, pretopology_cover
surjectiveFamiliesPretopology 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem_grothendieckTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.generate_bot CategoryTheory.Precoverage.generate_mem_toGrothendieck bot_mem_precoverage
exists_cover_of_mem_grothendieckTopology 📖	mathematical	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CategoryTheory.instCompleteLatticePresieve CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Sieve.arrows	—	mem_grothendieckTopology_iff
exists_cover_of_mem_pretopology 📖	mathematical	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Pretopology.toPrecoverage Pullback.instHasPullbacks pretopology	CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	Pullback.instHasPullbacks mem_pretopology_iff
grothendieckTopology_cover 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology CategoryTheory.Sieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	Cover.mem_grothendieckTopology
grothendieckTopology_eq_inf 📖	mathematical	—	grothendieckTopology CategoryTheory.Pretopology.toGrothendieck AlgebraicGeometry.Scheme instCategory Pullback.instHasPullbacks CategoryTheory.Pretopology SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Pretopology.instCompleteLattice jointlySurjectivePretopology CategoryTheory.MorphismProperty.pretopology	—	Pullback.instHasPullbacks grothendieckTopology.eq_1 instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight CategoryTheory.MorphismProperty.Respects.toRespectsLeft CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso CategoryTheory.MorphismProperty.Respects.toRespectsRight instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange isJointlySurjectivePreserving instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
grothendieckTopology_le_grothendieckTopology 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology grothendieckTopology	—	grothendieckTopology_monotone
grothendieckTopology_monotone 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology grothendieckTopology	—	CategoryTheory.Precoverage.toGrothendieck_mono precoverage_mono
instIsStableUnderBaseChangeJointlySurjectivePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderBaseChange AlgebraicGeometry.Scheme instCategory jointlySurjectivePrecoverage	—	CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage pullbackComparison_forget_surjective
jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology 📖	mathematical	—	jointlySurjectiveTopology CategoryTheory.Pretopology.toGrothendieck AlgebraicGeometry.Scheme instCategory Pullback.instHasPullbacks jointlySurjectivePretopology	—	CategoryTheory.GrothendieckTopology.copy_eq Pullback.instHasPullbacks
mem_grothendieckTopology_iff 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CategoryTheory.instCompleteLatticePresieve CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Sieve.arrows	—	instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange isJointlySurjectivePreserving instHasPullbacksPrecoverageOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks Pullback.instHasPullbacks instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight CategoryTheory.MorphismProperty.Respects.toRespectsLeft CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso CategoryTheory.MorphismProperty.Respects.toRespectsRight CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover le_trans instJointlySurjectivePrecoverage Cover.mem_pretopology
mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve jointlySurjectiveTopology CategoryTheory.Precoverage.coverings CategoryTheory.Pretopology.toPrecoverage Pullback.instHasPullbacks jointlySurjectivePretopology CategoryTheory.Sieve.arrows	—	—
mem_pretopology_iff 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Pretopology.toPrecoverage Pullback.instHasPullbacks pretopology CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover Pullback.instHasPullbacks
pretopology_cover 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Pretopology.toPrecoverage Pullback.instHasPullbacks pretopology CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	Cover.mem_pretopology
pretopology_eq_inf 📖	mathematical	—	pretopology CategoryTheory.Pretopology AlgebraicGeometry.Scheme instCategory Pullback.instHasPullbacks SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Pretopology.instCompleteLattice jointlySurjectivePretopology CategoryTheory.MorphismProperty.pretopology	—	Pullback.instHasPullbacks
pretopology_le_inf 📖	mathematical	—	pretopology CategoryTheory.Pretopology AlgebraicGeometry.Scheme instCategory Pullback.instHasPullbacks SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Pretopology.instCompleteLattice jointlySurjectivePretopology CategoryTheory.MorphismProperty.pretopology	—	pretopology_eq_inf
pretopology_le_pretopology 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Pretopology Pullback.instHasPullbacks CategoryTheory.Pretopology.LE pretopology	—	pretopology_monotone
pretopology_monotone 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.Pretopology Pullback.instHasPullbacks CategoryTheory.Pretopology.LE pretopology	—	precoverage_mono

AlgebraicGeometry.Scheme.Cover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_grothendieckTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve AlgebraicGeometry.Scheme.grothendieckTopology CategoryTheory.Sieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.generate_mem_toGrothendieck CategoryTheory.Precoverage.ZeroHypercover.mem₀
mem_pretopology 📖	mathematical	—	CategoryTheory.Presieve AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Pretopology.toPrecoverage AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.Scheme.pretopology CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.ZeroHypercover.mem₀

---

← Back to Index