ConstantSheaf

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

Statistics

Metric	Count
Definitions continuousMapPresheaf, continuousMapPresheafAb, continuousMapPresheafAbForgetIso, continuousMapPresheafEquivOfTotallyDisconnectedSpace, continuousMapPresheafIsoUlift	5
Theorems continuousMapPresheaf_map, continuousMapPresheaf_obj, isSheaf_fpqcTopology_continuousMapPresheaf, isSheaf_fpqcTopology_continuousMapPresheafAb, isSheaf_zariskiTopology_continuousMapPresheaf	5
Total	10

AlgebraicGeometry

Definitions

Name	Category	Theorems
continuousMapPresheaf 📖	CompOp	4 math math: continuousMapPresheaf_obj, continuousMapPresheaf_map, isSheaf_fpqcTopology_continuousMapPresheaf, isSheaf_zariskiTopology_continuousMapPresheaf
continuousMapPresheafAb 📖	CompOp	1 math math: isSheaf_fpqcTopology_continuousMapPresheafAb
continuousMapPresheafAbForgetIso 📖	CompOp	—
continuousMapPresheafEquivOfTotallyDisconnectedSpace 📖	CompOp	—
continuousMapPresheafIsoUlift 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMapPresheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite Scheme CategoryTheory.Category.opposite Scheme.instCategory CategoryTheory.types continuousMapPresheaf ContinuousMap.comp TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Opposite.unop SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.Hom.hom PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
continuousMapPresheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite Scheme CategoryTheory.Category.opposite Scheme.instCategory CategoryTheory.types continuousMapPresheaf ContinuousMap TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Opposite.unop SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
isSheaf_fpqcTopology_continuousMapPresheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Scheme Scheme.instCategory CategoryTheory.types Scheme.fpqcTopology continuousMapPresheaf	—	CategoryTheory.isSheaf_iff_isSheaf_of_type Scheme.fpqcTopology_eq_propQCTopology isSheaf_type_propQCTopology_iff Flat.isStableUnderBaseChange Flat.instIsMultiplicativeScheme HasRingHomProperty.instIsZariskiLocalAtSource Flat.instHasRingHomPropertyFlat isSheaf_zariskiTopology_continuousMapPresheaf CategoryTheory.Presieve.isSheafFor_singleton Flat.isQuotientMap_of_surjective instQuasiCompactOfIsAffineHom isAffineHom_of_isAffine isAffine_Spec Scheme.Pullback.instHasPullback Scheme.Pullback.exists_preimage_pullback CategoryTheory.Limits.pullback.condition Topology.IsQuotientMap.lift_comp ContinuousMap.cancel_right Scheme.Hom.surjective
isSheaf_fpqcTopology_continuousMapPresheafAb 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Scheme Scheme.instCategory Ab AddCommGrpCat.instCategory Scheme.fpqcTopology continuousMapPresheafAb	—	CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp CategoryTheory.reflectsLimitsOfCreatesLimits isSheaf_fpqcTopology_continuousMapPresheaf
isSheaf_zariskiTopology_continuousMapPresheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf Scheme Scheme.instCategory CategoryTheory.types Scheme.zariskiTopology continuousMapPresheaf	—	CategoryTheory.Presheaf.isSheaf_of_iso_iff CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf Scheme.instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology TopCat.instIsContinuousUliftFunctorGrothendieckTopology CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable TopCat.subcanonical_grothendieckTopology CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda

---

← Back to Index