SmallAffineZariski

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

Statistics

Metric	Count
Definitions AffineZariskiSite, PreservesLocalization, basicOpen, cocone, directedCover, grothendieckTopology, instLocallyDirectedIsOpenImmersionDirectedCover, instPartialOrder, instPreorder, isColimitCocone, presieveOfSections, relativeGluingData, restrictIsoSpec, sectionsOfPresieve, sheafEquiv, toOpens, toOpensFunctor	17
Theorems colimitDesc_preimage, isLocallyDirected, isOpenImmersion, opensRange_map, basicOpen_coe, basicOpen_le, cocone_pt, cocone_ι_app, coequifibered_iff_forall_isLocalizationAway, directedCover_I₀, directedCover_X, directedCover_f, generate_presieveOfSections, generate_presieveOfSections_mem_grothendieckTopology, instFaithfulOpensToOpensFunctor, instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, mem_grothendieckTopology, mem_grothendieckTopology_iff_sectionsOfPresieve, opensRange_relativeGluingData_map, presieveOfSections_eq_ofArrows, presieveOfSections_sectionsOfPresieve, presieveOfSections_surjective, restrictIsoSpec_hom_app, restrictIsoSpec_inv_app, toOpensFunctor_obj, toOpens_injective, toOpens_mono, preservesLocalization_toOpensFunctor	30
Total	47

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
AffineZariskiSite 📖	CompOp	22 math math: AffineZariskiSite.instFaithfulOpensToOpensFunctor, AffineZariskiSite.basicOpen_le, AffineZariskiSite.generate_presieveOfSections, Hom.coequifibered_normalizationDiagramMap, AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AffineZariskiSite.restrictIsoSpec_hom_app, AffineZariskiSite.presieveOfSections_surjective, AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, Hom.preservesLocalization_normalizationDiagramMap, AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, AffineZariskiSite.toOpens_mono, AffineZariskiSite.mem_grothendieckTopology, AffineZariskiSite.toOpens_injective, AffineZariskiSite.cocone_ι_app, AffineZariskiSite.cocone_pt, AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AffineZariskiSite.presieveOfSections_eq_ofArrows, AffineZariskiSite.directedCover_I₀, AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AffineZariskiSite.toOpensFunctor_obj, AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AffineZariskiSite.restrictIsoSpec_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLocalization_toOpensFunctor 📖	mathematical	—	CategoryTheory.NatTrans.Coequifibered	—	CategoryTheory.NatTrans.Coequifibered.of_isIso

AlgebraicGeometry.Scheme.AffineZariskiSite

Definitions

Name	Category	Theorems
PreservesLocalization 📖	CompOp	—
basicOpen 📖	CompOp	6 math math: basicOpen_le, coequifibered_iff_forall_isLocalizationAway, opensRange_relativeGluingData_map, PreservesLocalization.opensRange_map, basicOpen_coe, presieveOfSections_eq_ofArrows
cocone 📖	CompOp	2 math math: cocone_ι_app, cocone_pt
directedCover 📖	CompOp	7 math math: directedCover_X, directedCover_f, opensRange_relativeGluingData_map, PreservesLocalization.opensRange_map, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, PreservesLocalization.colimitDesc_preimage, directedCover_I₀
grothendieckTopology 📖	CompOp	4 math math: generate_presieveOfSections_mem_grothendieckTopology, instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, mem_grothendieckTopology, mem_grothendieckTopology_iff_sectionsOfPresieve
instLocallyDirectedIsOpenImmersionDirectedCover 📖	CompOp	4 math math: opensRange_relativeGluingData_map, PreservesLocalization.opensRange_map, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, PreservesLocalization.colimitDesc_preimage
instPartialOrder 📖	CompOp	—
instPreorder 📖	CompOp	21 math math: instFaithfulOpensToOpensFunctor, basicOpen_le, generate_presieveOfSections, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, generate_presieveOfSections_mem_grothendieckTopology, restrictIsoSpec_hom_app, presieveOfSections_surjective, coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, toOpens_mono, mem_grothendieckTopology, cocone_ι_app, cocone_pt, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, presieveOfSections_eq_ofArrows, mem_grothendieckTopology_iff_sectionsOfPresieve, toOpensFunctor_obj, instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, restrictIsoSpec_inv_app
isColimitCocone 📖	CompOp	—
presieveOfSections 📖	CompOp	5 math math: generate_presieveOfSections, generate_presieveOfSections_mem_grothendieckTopology, presieveOfSections_surjective, presieveOfSections_sectionsOfPresieve, presieveOfSections_eq_ofArrows
relativeGluingData 📖	CompOp	3 math math: opensRange_relativeGluingData_map, PreservesLocalization.opensRange_map, PreservesLocalization.colimitDesc_preimage
restrictIsoSpec 📖	CompOp	2 math math: restrictIsoSpec_hom_app, restrictIsoSpec_inv_app
sectionsOfPresieve 📖	CompOp	2 math math: presieveOfSections_sectionsOfPresieve, mem_grothendieckTopology_iff_sectionsOfPresieve
sheafEquiv 📖	CompOp	—
toOpens 📖	CompOp	12 math math: generate_presieveOfSections, generate_presieveOfSections_mem_grothendieckTopology, restrictIsoSpec_hom_app, presieveOfSections_surjective, toOpens_mono, mem_grothendieckTopology, toOpens_injective, basicOpen_coe, presieveOfSections_eq_ofArrows, mem_grothendieckTopology_iff_sectionsOfPresieve, toOpensFunctor_obj, restrictIsoSpec_inv_app
toOpensFunctor 📖	CompOp	12 math math: instFaithfulOpensToOpensFunctor, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, restrictIsoSpec_hom_app, coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, cocone_ι_app, cocone_pt, instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, toOpensFunctor_obj, instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, restrictIsoSpec_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_coe 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.IsAffineOpen basicOpen AlgebraicGeometry.Scheme.basicOpen toOpens	—	—
basicOpen_le 📖	mathematical	—	AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.toLE instPreorder basicOpen	—	—
cocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp TopologicalSpace.Opens TopCat.str AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Spec cocone	—	—
cocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp TopologicalSpace.Opens TopCat.str AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι cocone AlgebraicGeometry.IsAffineOpen.fromSpec AlgebraicGeometry.IsAffineOpen	—	—
coequifibered_iff_forall_isLocalizationAway 📖	mathematical	—	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf IsLocalization.Away CommRingCat.carrier CategoryTheory.Functor.obj Opposite.op CommRing.toCommSemiring CommRingCat.commRing DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app basicOpen RingHom.toAlgebra CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE basicOpen_le	—	AlgebraicGeometry.Scheme.basicOpen_le basicOpen_le IsScalarTower.of_algebraMap_eq' CategoryTheory.NatTrans.naturality AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen CommRingCat.isPushout_iff_isPushout Algebra.IsPushout.comm Algebra.isLocalization_iff_isPushout Algebra.algebraMapSubmonoid_powers
directedCover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion directedCover AlgebraicGeometry.Scheme.AffineZariskiSite	—	—
directedCover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion directedCover AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.IsAffineOpen	—	—
directedCover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion directedCover AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.IsAffineOpen	—	—
generate_presieveOfSections 📖	mathematical	—	CategoryTheory.Sieve.arrows AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder CategoryTheory.Sieve.generate presieveOfSections CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens toOpens Set Set.instMembership AlgebraicGeometry.Scheme.basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing	—	AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen AlgebraicGeometry.Scheme.basicOpen_mul inf_eq_right AlgebraicGeometry.Scheme.basicOpen_le le_trans le_refl AlgebraicGeometry.Scheme.basicOpen_res
generate_presieveOfSections_mem_grothendieckTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology CategoryTheory.Sieve.generate presieveOfSections Ideal.span CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens toOpens CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff mem_grothendieckTopology SetLike.le_def instIsConcreteLE isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_coe_set Set.iUnion_congr_Prop AlgebraicGeometry.Scheme.basicOpen_mul mul_one
instFaithfulOpensToOpensFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor	—	Preorder.subsingleton_hom
instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat 📖	mathematical	—	CategoryTheory.Functor.IsCoverDense AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor Opens.grothendieckTopology	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open AlgebraicGeometry.Scheme.isBasis_affineOpens TopologicalSpace.Opens.is_open'
instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor 📖	mathematical	—	CategoryTheory.Functor.IsDenseSubsite AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder grothendieckTopology Opens.grothendieckTopology toOpensFunctor	—	instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOpensToOpensFunctor
instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat 📖	mathematical	—	CategoryTheory.Functor.IsLocallyFull AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor Opens.grothendieckTopology	—	AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le AlgebraicGeometry.Scheme.basicOpen_res inf_eq_right
mem_grothendieckTopology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology CategoryTheory.Sieve.arrows TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpens	—	toOpens_mono
mem_grothendieckTopology_iff_sectionsOfPresieve 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve grothendieckTopology Ideal.span CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens toOpens CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing sectionsOfPresieve CategoryTheory.Sieve.arrows Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	generate_presieveOfSections_mem_grothendieckTopology presieveOfSections_sectionsOfPresieve CategoryTheory.Sieve.generate_sieve
opensRange_relativeGluingData_map 📖	mathematical	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf	AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Functor.obj CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion directedCover AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor instLocallyDirectedIsOpenImmersionDirectedCover relativeGluingData basicOpen CategoryTheory.Functor.map CategoryTheory.homOfLE basicOpen_le AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor PrimeSpectrum.basicOpen CommRingCat.carrier Opposite.op CommRing.toCommSemiring CommRingCat.commRing DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app	—	basicOpen_le coequifibered_iff_forall_isLocalizationAway AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor PrimeSpectrum.localization_away_comap_range
presieveOfSections_eq_ofArrows 📖	mathematical	—	presieveOfSections CategoryTheory.Presieve.ofArrows AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder Set.Elem CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens toOpens basicOpen Set Set.instMembership CategoryTheory.homOfLE basicOpen_le	—	basicOpen_le
presieveOfSections_sectionsOfPresieve 📖	mathematical	—	presieveOfSections sectionsOfPresieve	—	—
presieveOfSections_surjective 📖	mathematical	—	Set CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens toOpens CategoryTheory.Presieve AlgebraicGeometry.Scheme.AffineZariskiSite instPreorder presieveOfSections	—	presieveOfSections_sectionsOfPresieve
restrictIsoSpec_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor CategoryTheory.Over CategoryTheory.instCategoryOver AlgebraicGeometry.Scheme.restrictFunctor CategoryTheory.Over.forget Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp TopologicalSpace.Opens TopCat.str AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Spec CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictIsoSpec AlgebraicGeometry.Scheme.Opens.toScheme toOpens AlgebraicGeometry.Spec CategoryTheory.Functor.obj Opposite.op AlgebraicGeometry.IsAffineOpen.isoSpec AlgebraicGeometry.IsAffineOpen	—	—
restrictIsoSpec_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp TopologicalSpace.Opens TopCat.str AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Spec CategoryTheory.Over CategoryTheory.instCategoryOver AlgebraicGeometry.Scheme.restrictFunctor CategoryTheory.Over.forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictIsoSpec AlgebraicGeometry.Scheme.Opens.toScheme toOpens AlgebraicGeometry.Spec CategoryTheory.Functor.obj Opposite.op AlgebraicGeometry.IsAffineOpen.isoSpec AlgebraicGeometry.IsAffineOpen	—	—
toOpensFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.AffineZariskiSite Preorder.smallCategory instPreorder AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpensFunctor toOpens	—	—
toOpens_injective 📖	mathematical	—	AlgebraicGeometry.Scheme.AffineZariskiSite AlgebraicGeometry.Scheme.Opens toOpens	—	Subtype.val_injective
toOpens_mono 📖	mathematical	—	Monotone AlgebraicGeometry.Scheme.AffineZariskiSite AlgebraicGeometry.Scheme.Opens instPreorder PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier toOpens	—	AlgebraicGeometry.Scheme.basicOpen_le

AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitDesc_preimage 📖	mathematical	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.AffineZariskiSite.instLocallyDirectedIsOpenImmersionDirectedCover AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData UnivLE.small UnivLE.self Preorder.subsingleton_hom TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase AlgebraicGeometry.IsAffineOpen AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF	—	UnivLE.small UnivLE.self Preorder.subsingleton_hom AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι AlgebraicGeometry.Scheme.Opens.opensRange_ι AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι
isLocallyDirected 📖	mathematical	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf	CategoryTheory.Functor.IsLocallyDirected AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Spec AlgebraicGeometry.Scheme.forget	—	AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin Preorder.subsingleton_hom
isOpenImmersion 📖	mathematical	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.map	—	AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor
opensRange_map 📖	mathematical	CategoryTheory.NatTrans.Coequifibered Opposite AlgebraicGeometry.Scheme.AffineZariskiSite CommRingCat CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.op AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor AlgebraicGeometry.PresheafedSpace.presheaf	AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Functor.obj CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor AlgebraicGeometry.Scheme.AffineZariskiSite.instLocallyDirectedIsOpenImmersionDirectedCover AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen CategoryTheory.Functor.map CategoryTheory.homOfLE AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor PrimeSpectrum.basicOpen CommRingCat.carrier Opposite.op CommRing.toCommSemiring CommRingCat.commRing DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app	—	AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map

---

← Back to Index