Open

📁 Source: Mathlib/AlgebraicGeometry/Cover/Open.lean

Statistics

Metric	Count
Definitions AffineOpenCover, openCover, affineRefinement, finiteSubcover, fromAffineRefinement, pullbackCoverAffineRefinementObjIso, affineBasisCover, affineBasisCoverOfAffine, affineBasisCoverRing, affineCover, affineOpenCover, affineOpenCoverOfSpanRangeEqTop, instFintypeI₀FiniteSubcover, instInhabitedOpenCover	14
Theorems instIsOpenImmersionF, openCover_I₀, openCover_X, openCover_f, compactSpace, ext_elem, finiteSubcover_X, finiteSubcover_f, iSup_opensRange, isOpenCover_opensRange, pullbackCoverAffineRefinementObjIso_inv_map, pullbackCoverAffineRefinementObjIso_inv_map_assoc, pullbackCoverAffineRefinementObjIso_inv_pullbackHom, pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, affineBasisCover_is_basis, affineBasisCover_map_range, affineBasisCover_obj, affineOpenCoverOfSpanRangeEqTop_I₀, affineOpenCoverOfSpanRangeEqTop_X_carrier, affineOpenCoverOfSpanRangeEqTop_f, affineOpenCoverOfSpanRangeEqTop_idx, affineOpenCover_I₀, affineOpenCover_X, affineOpenCover_f, affineOpenCover_idx, instHasPullbacksIsOpenImmersion, instIsOpenImmersionF, isNilpotent_of_isNilpotent_cover, openCover_affineOpenCover, zero_of_zero_cover	30
Total	44

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
AffineOpenCover 📖	CompOp	—
affineBasisCover 📖	CompOp	4 math math: affineBasisCover_is_basis, isAffine_affineBasisCover, affineBasisCover_obj, affineBasisCover_map_range
affineBasisCoverOfAffine 📖	CompOp	—
affineBasisCoverRing 📖	CompOp	1 math math: affineBasisCover_obj
affineCover 📖	CompOp	12 math math: affineOpenCover_I₀, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, affineOpenCover_idx, Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.instIsAffineXSchemeAffineCover, OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, affineOpenCover_f, affineBasisCover_map_range, openCover_affineOpenCover, isAffine_affineCover
affineOpenCover 📖	CompOp	5 math math: affineOpenCover_I₀, affineOpenCover_idx, affineOpenCover_f, openCover_affineOpenCover, affineOpenCover_X
affineOpenCoverOfSpanRangeEqTop 📖	CompOp	4 math math: affineOpenCoverOfSpanRangeEqTop_X_carrier, affineOpenCoverOfSpanRangeEqTop_idx, affineOpenCoverOfSpanRangeEqTop_f, affineOpenCoverOfSpanRangeEqTop_I₀
instFintypeI₀FiniteSubcover 📖	CompOp	—
instInhabitedOpenCover 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineBasisCover_is_basis 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier setOf Set CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion affineBasisCover Set.range CategoryTheory.PreZeroHypercover.X DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds AlgebraicGeometry.IsOpenImmersion.isOpen_range instIsOpenImmersionF instJointlySurjectivePrecoverage Cover.covers local_affine TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isBasis_basic_opens Continuous.isOpen_preimage Hom.continuous TopologicalSpace.OpenNhds.isOpenEmbedding affineBasisCover_map_range Set.image_subset_iff
affineBasisCover_map_range 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion affineBasisCover CategoryTheory.PreZeroHypercover.I₀ affineCover DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f Set.image TopologicalSpace.Opens.carrier PrimeSpectrum CommRingCat.carrier CategoryTheory.Iso AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens AlgebraicGeometry.LocallyRingedSpace.toTopCat Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.toTopCat SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.OpenNhds TopologicalSpace.Opens.inclusion' TopologicalSpace.OpenNhds.isOpenEmbedding Opposite CategoryTheory.Category.opposite AlgebraicGeometry.Spec.toLocallyRingedSpace Opposite.op local_affine CommRing.toCommSemiring CommRingCat.commRing PrimeSpectrum.zariskiTopology PrimeSpectrum.basicOpen	—	TopologicalSpace.OpenNhds.isOpenEmbedding local_affine Set.range_comp Set.image_congr PrimeSpectrum.localization_away_comap_range Localization.isLocalization
affineBasisCover_obj 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion affineBasisCover AlgebraicGeometry.Spec affineBasisCoverRing	—	—
affineOpenCoverOfSpanRangeEqTop_I₀ 📖	mathematical	Ideal.span CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	AffineCover.I₀ AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec affineOpenCoverOfSpanRangeEqTop	—	—
affineOpenCoverOfSpanRangeEqTop_X_carrier 📖	mathematical	Ideal.span CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	AffineCover.X AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec affineOpenCoverOfSpanRangeEqTop Localization.Away CommRing.toCommMonoid	—	—
affineOpenCoverOfSpanRangeEqTop_f 📖	mathematical	Ideal.span CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	AffineCover.f AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec affineOpenCoverOfSpanRangeEqTop AlgebraicGeometry.Spec.map CommRingCat.of Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm CommRingCat.ofHom algebraMap OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instAlgebra Algebra.id	—	—
affineOpenCoverOfSpanRangeEqTop_idx 📖	mathematical	Ideal.span CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	AffineCover.idx AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec affineOpenCoverOfSpanRangeEqTop	—	—
affineOpenCover_I₀ 📖	mathematical	—	AffineCover.I₀ AlgebraicGeometry.IsOpenImmersion affineOpenCover CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage affineCover	—	—
affineOpenCover_X 📖	mathematical	—	AffineCover.X AlgebraicGeometry.IsOpenImmersion affineOpenCover CommRingCat CategoryTheory.Iso AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.Opens.inclusion' Opposite CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace Opposite.op	—	—
affineOpenCover_f 📖	mathematical	—	AffineCover.f AlgebraicGeometry.IsOpenImmersion affineOpenCover CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage affineCover	—	—
affineOpenCover_idx 📖	mathematical	—	AffineCover.idx AlgebraicGeometry.IsOpenImmersion affineOpenCover CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage affineCover TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.PreZeroHypercover.X DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f	—	—
instHasPullbacksIsOpenImmersion 📖	mathematical	—	CategoryTheory.MorphismProperty.HasPullbacks AlgebraicGeometry.Scheme instCategory AlgebraicGeometry.IsOpenImmersion	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left
instIsOpenImmersionF 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.f	—	Cover.map_prop
isNilpotent_of_isNilpotent_cover 📖	—	IsNilpotent CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.app	—	—	Finset.le_sup Finset.mem_univ zero_of_zero_cover map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass pow_eq_zero_of_le
openCover_affineOpenCover 📖	mathematical	—	AffineOpenCover.openCover affineOpenCover affineCover	—	—
zero_of_zero_cover 📖	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Hom.app MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	OpenCover.ext_elem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

AlgebraicGeometry.Scheme.AffineOpenCover

Definitions

Name	Category	Theorems
openCover 📖	CompOp	9 math math: openCover_f, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, openCover_I₀, AlgebraicGeometry.Scheme.openCover_affineOpenCover, openCover_X, AlgebraicGeometry.Scheme.isAffine_affineOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOpenImmersionF 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X AlgebraicGeometry.Scheme.AffineCover.f	—	AlgebraicGeometry.Scheme.AffineCover.map_prop
openCover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover AlgebraicGeometry.Scheme.AffineCover.I₀	—	—
openCover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X	—	—
openCover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover AlgebraicGeometry.Scheme.AffineCover.f	—	—

AlgebraicGeometry.Scheme.OpenCover

Definitions

Name	Category	Theorems
affineRefinement 📖	CompOp	4 math math: pullbackCoverAffineRefinementObjIso_inv_pullbackHom, pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, pullbackCoverAffineRefinementObjIso_inv_map, pullbackCoverAffineRefinementObjIso_inv_map_assoc
finiteSubcover 📖	CompOp	3 math math: AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover, finiteSubcover_f, finiteSubcover_X
fromAffineRefinement 📖	CompOp	—
pullbackCoverAffineRefinementObjIso 📖	CompOp	4 math math: pullbackCoverAffineRefinementObjIso_inv_pullbackHom, pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, pullbackCoverAffineRefinementObjIso_inv_map, pullbackCoverAffineRefinementObjIso_inv_map_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	—	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—	nonempty_fintype isCompact_univ_iff AlgebraicGeometry.Scheme.Cover.iUnion_range AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage isCompact_iUnion isCompact_iff_compactSpace Homeomorph.compactSpace Topology.IsOpenEmbedding.isOpen_range AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.Scheme.Cover.map_prop TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.ofRestrict Subtype.range_coe AlgebraicGeometry.Scheme.Hom.isIso_base CategoryTheory.Iso.isIso_hom
ext_elem 📖	—	DFunLike.coe 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 CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.app	—	—	TopCat.Sheaf.eq_of_locally_eq' CommRingCat.hasLimits CommRingCat.forgetReflectIsos CommRingCat.forget_preservesLimits AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.instIsOpenImmersionF inf_le_right isOpen_iUnion TopologicalSpace.Opens.is_open' AlgebraicGeometry.Scheme.Cover.covers RingEquiv.injective AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv
finiteSubcover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion finiteSubcover AlgebraicGeometry.Scheme.Cover.idx AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Finset SetLike.instMembership Finset.instSetLike Set Set.iUnion Finset.instMembership Set.range DFunLike.coe ContinuousMap TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.PreZeroHypercover.f Set.univ	—	AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage
finiteSubcover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion finiteSubcover AlgebraicGeometry.Scheme.Cover.idx AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Finset SetLike.instMembership Finset.instSetLike Set Set.iUnion Finset.instMembership Set.range CategoryTheory.PreZeroHypercover.X DFunLike.coe ContinuousMap TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Set.univ	—	AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage
iSup_opensRange 📖	mathematical	—	iSup AlgebraicGeometry.Scheme.Opens CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.ext AlgebraicGeometry.Scheme.instIsOpenImmersionF TopologicalSpace.Opens.coe_iSup AlgebraicGeometry.Scheme.Cover.iUnion_range AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage
isOpenCover_opensRange 📖	mathematical	—	TopologicalSpace.IsOpenCover CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF	—	AlgebraicGeometry.Scheme.instIsOpenImmersionF iSup_opensRange
pullbackCoverAffineRefinementObjIso_inv_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme.Cover.pullbackHom AlgebraicGeometry.Scheme.affineCover AlgebraicGeometry.Scheme.AffineOpenCover.openCover affineRefinement CategoryTheory.Iso.inv pullbackCoverAffineRefinementObjIso	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc
pullbackCoverAffineRefinementObjIso_inv_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme.affineCover AlgebraicGeometry.Scheme.Cover.pullbackHom AlgebraicGeometry.Scheme.AffineOpenCover.openCover affineRefinement CategoryTheory.Iso.inv pullbackCoverAffineRefinementObjIso	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackCoverAffineRefinementObjIso_inv_map
pullbackCoverAffineRefinementObjIso_inv_pullbackHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme.Cover.pullbackHom AlgebraicGeometry.Scheme.affineCover AlgebraicGeometry.Scheme.AffineOpenCover.openCover affineRefinement CategoryTheory.Iso.inv pullbackCoverAffineRefinementObjIso	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst
pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme.affineCover AlgebraicGeometry.Scheme.Cover.pullbackHom AlgebraicGeometry.Scheme.AffineOpenCover.openCover affineRefinement CategoryTheory.Iso.inv pullbackCoverAffineRefinementObjIso	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackCoverAffineRefinementObjIso_inv_pullbackHom

---

← Back to Index