AffineTransitionLimit

📁 Source: Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

Statistics

Metric	Count
Definitions ExistsHomHomCompEqCompAux, D', a, b, c, c', g, hc, hc', hii', i, i', 𝒰D, 𝒰D₀, 𝒰S, 𝒰X, isLimitOpensCone, opensCone, opensDiagram, opensDiagramι	20
Theorems exists_eq, exists_index, ha, hab, hb, h𝒰S, h𝒰X, range_g_subset, compactSpace_of_isLimit, exists_hom_comp_eq_comp_of_locallyOfFiniteType, exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType, exists_isAffine_of_isLimit, exists_isOpenCover_and_isAffine, exists_isQuasiAffine_of_isLimit, exists_π_app_comp_eq_of_locallyOfFinitePresentation, nonempty_of_isLimit, exists_appTop_map_eq_zero_of_isAffine_of_isLimit, exists_appTop_map_eq_zero_of_isLimit, exists_appTop_π_eq_of_isAffine_of_isLimit, exists_appTop_π_eq_of_isLimit, exists_app_map_eq_map_of_isLimit, exists_app_map_eq_zero_of_isLimit, exists_isAffineOpen_preimage_eq, exists_map_eq_top, exists_map_preimage_eq_map_preimage, exists_map_preimage_le_map_preimage, exists_mem_of_isClosed_of_nonempty, exists_mem_of_isClosed_of_nonempty', exists_preimage_eq, instIsAffineHomMapOverSchemeOpensDiagram, instIsOpenImmersionAppOverSchemeOpensDiagramι, instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj, isAffineHom_π_app, isBasis_preimage_isAffineOpen, nonempty_isColimit_Γ_mapCocone, opensCone_pt, opensCone_π_app, opensDiagram_map, opensDiagram_obj, opensDiagramι_app	40
Total	60

AlgebraicGeometry

Definitions

Name	Category	Theorems
ExistsHomHomCompEqCompAux 📖	CompData	—
isLimitOpensCone 📖	CompOp	—
opensCone 📖	CompOp	2 math math: opensCone_pt, opensCone_π_app
opensDiagram 📖	CompOp	7 math math: opensCone_pt, opensDiagram_map, opensDiagramι_app, instIsAffineHomMapOverSchemeOpensDiagram, opensDiagram_obj, opensCone_π_app, instIsOpenImmersionAppOverSchemeOpensDiagramι
opensDiagramι 📖	CompOp	2 math math: opensDiagramι_app, instIsOpenImmersionAppOverSchemeOpensDiagramι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_appTop_map_eq_zero_of_isAffine_of_isLimit 📖	mathematical	IsAffine CategoryTheory.Functor.obj Scheme Scheme.instCategory DFunLike.coe Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	CategoryTheory.Functor.map	—	CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty CategoryTheory.Limits.comp_preservesColimit preservesColimit_Γ CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
exists_appTop_map_eq_zero_of_isLimit 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map DFunLike.coe Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	le_top TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ IsAffineOpen.preimage exists_appTop_map_eq_zero_of_isAffine_of_isLimit CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty Scheme.Opens.instIsOpenImmersionι LE.le.trans Scheme.Hom.le_resLE_preimage_iff le_rfl Set.image_subset_iff Scheme.Hom.app_eq_appLE Scheme.Hom.resLE_appLE Scheme.Opens.ι_appLE Scheme.Hom.map_appLE Scheme.Hom.appLE_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass CategoryTheory.Category.comp_id CategoryTheory.Over.w Scheme.Opens.ι_image_top Set.image_preimage_subset Scheme.Hom.resLE.congr_simp CategoryTheory.eqToHom_op CompactSpace.elim_nhds_subcover IsOpen.mem_nhds TopologicalSpace.Opens.is_open' Finset.mem_insert_of_mem Finset.mem_image_of_mem CategoryTheory.IsCofiltered.inf_exists TopCat.Presheaf.IsSheaf.section_ext CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos SheafedSpace.IsSheaf Set.mem_iUnion₂ Eq.ge Finset.mem_image Finset.mem_insert_self Scheme.Hom.comp_preimage CategoryTheory.Functor.map_comp le_refl Scheme.Hom.appLE_comp_appLE Scheme.Hom.appLE.congr_simp
exists_appTop_π_eq_of_isAffine_of_isLimit 📖	mathematical	IsAffine CategoryTheory.Functor.obj Scheme Scheme.instCategory	DFunLike.coe Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.comp_preservesColimit preservesColimit_Γ CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered
exists_appTop_π_eq_of_isLimit 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace	DFunLike.coe Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	Scheme.compactSpace_of_isLimit le_top CategoryTheory.IsCofiltered.nonempty TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ IsAffineOpen.preimage exists_appTop_π_eq_of_isAffine_of_isLimit CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty Scheme.Opens.instIsOpenImmersionι Scheme.Hom.image_top_eq_opensRange Scheme.Opens.opensRange_ι CategoryTheory.Limits.Cone.w le_rfl LE.le.trans Scheme.Hom.le_resLE_preimage_iff Scheme.Hom.app_eq_appLE Scheme.Hom.resLE_appLE Scheme.Hom.appLE_map CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp inf_le_left inf_le_right CategoryTheory.IsCofilteredOrEmpty.cone_objs exists_app_map_eq_zero_of_isLimit IsCompact.inter_of_isOpen IsAffineOpen.isCompact IsOpen.preimage Scheme.Hom.continuous TopologicalSpace.Opens.is_open' map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Scheme.Hom.appLE_comp_appLE Scheme.Hom.appLE.congr_simp le_refl map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CompactSpace.elim_nhds_subcover IsOpen.mem_nhds Finset.subset_union_left Finset.mem_image_of_mem Finset.subset_union_right Finset.mem_image₂_of_mem CategoryTheory.IsCofiltered.inf_exists Finset.mem_image₂ exists_map_eq_top SetLike.coe_injective ContinuousMap.continuous isOpen_iUnion Set.iUnion_congr_Prop Set.preimage_iUnion CategoryTheory.Presheaf.IsSheaf.isSheafFor CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos SheafedSpace.IsSheaf Eq.ge CategoryTheory.Presieve.isSheafFor_arrows_iff CategoryTheory.Presieve.isSheafFor_iff_generate CategoryTheory.Category.assoc le_inf_iff TopCat.Presheaf.section_ext CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.FilteredColimits.forget_preservesFilteredColimits TopCat.Presheaf.germ_ext Scheme.Hom.comp_preimage CategoryTheory.Limits.Cone.w_assoc Scheme.Hom.map_appLE Set.mem_iUnion₂
exists_app_map_eq_map_of_isLimit 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsCompact TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe Scheme.Opens TopologicalSpace.Opens.instSetLike DFunLike.coe Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.app	—	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass exists_app_map_eq_zero_of_isLimit
exists_app_map_eq_zero_of_isLimit 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsCompact TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe Scheme.Opens TopologicalSpace.Opens.instSetLike DFunLike.coe Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.app MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	isCompact_iff_compactSpace CategoryTheory.Functor.map_id TopologicalSpace.Opens.map_id_obj Scheme.Opens.instIsOpenImmersionι Scheme.Hom.image_top_eq_opensRange Scheme.Opens.opensRange_ι exists_appTop_map_eq_zero_of_isLimit CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty instIsAffineHomMapOverSchemeOpensDiagram map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass CategoryTheory.ConcreteCategory.comp_apply LE.le.trans Scheme.Hom.le_resLE_preimage_iff le_rfl Scheme.Hom.app_eq_appLE Scheme.Hom.resLE_appLE Scheme.Hom.map_appLE Scheme.Hom.appLE_map CategoryTheory.Category.comp_id CategoryTheory.Over.w
exists_isAffineOpen_preimage_eq 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map QuasiSeparatedSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	IsAffineOpen Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	exists_preimage_eq IsAffineOpen.isCompact isCompact_iff_compactSpace QuasiCompact.isCompact_preimage instQuasiCompactOfIsAffineHom TopologicalSpace.Opens.is_open' isQuasiSeparated_iff_quasiSeparatedSpace IsQuasiSeparated.of_quasiSeparatedSpace Scheme.exists_isAffine_of_isLimit CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty instIsAffineHomMapOverSchemeOpensDiagram Scheme.Hom.comp_preimage CategoryTheory.Limits.Cone.w
exists_map_eq_top 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—	exists_mem_of_isClosed_of_nonempty' CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty IsOpen.isClosed_compl TopologicalSpace.Opens.is_open' SetLike.coe_injective IsClosed.isCompact CategoryTheory.Functor.map_comp Eq.ge Set.mem_univ CategoryTheory.Functor.map_id TopologicalSpace.Opens.map_id_obj
exists_map_preimage_eq_map_preimage 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsCompact TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.smallCategory TopologicalSpace.Opens TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—	exists_map_preimage_le_map_preimage Eq.le Eq.ge CategoryTheory.IsCofiltered.cospan CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty le_antisymm CategoryTheory.Functor.map_comp Scheme.Hom.preimage_mono
exists_map_preimage_le_map_preimage 📖	—	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsCompact TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe Scheme.Opens TopologicalSpace.Opens.instSetLike CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—	isCompact_iff_compactSpace QuasiCompact.isCompact_preimage instQuasiCompactOfIsAffineHom TopologicalSpace.Opens.is_open' Scheme.Hom.comp_preimage top_le_iff LE.le.trans Scheme.Opens.ι_preimage_self Scheme.Hom.preimage_mono CategoryTheory.Functor.map_id TopologicalSpace.Opens.map_id_obj exists_map_eq_top CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty instIsAffineHomMapOverSchemeOpensDiagram Scheme.isoOfEq_hom_ι Scheme.Hom.resLE_comp_ι Scheme.Opens.instIsOpenImmersionι Set.image_subset_iff Eq.ge Scheme.Hom.image_top_eq_opensRange Scheme.Opens.opensRange_ι CategoryTheory.Category.comp_id CategoryTheory.Discrete.functor_map_id CategoryTheory.CommaMorphism.w
exists_mem_of_isClosed_of_nonempty 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsClosed TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Set.Nonempty IsCompact Set.MapsTo DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	Set Set.instMembership CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	Scheme.IdealSheafData.map_vanishingIdeal Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal Set.image_congr Set.MapsTo.subset_preimage CategoryTheory.Functor.map_id Scheme.IdealSheafData.subschemeMap.congr_simp CategoryTheory.cancel_mono IsPreimmersion.instMonoScheme Scheme.IdealSheafData.instIsPreimmersionSubschemeι Scheme.IdealSheafData.subschemeMap_subschemeι CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Scheme.IdealSheafData.subschemeMap_subschemeι_assoc le_iSup_of_le CategoryTheory.Limits.Cone.w IsClosedImmersion.instSubschemeι LE.le.trans Scheme.IdealSheafData.ker_subschemeι Scheme.Hom.le_ker_comp CategoryTheory.Limits.IsLimit.fac IsClosedImmersion.lift_fac_assoc CategoryTheory.Limits.IsLimit.hom_ext IsClosedImmersion.lift_fac Scheme.nonempty_of_isLimit instIsAffineHomCompScheme IsClosedImmersion.instIsAffineHom IsAffineHom.of_comp IsSeparated.isSeparated_of_mono Set.nonempty_coe_sort isCompact_iff_compactSpace Scheme.Hom.continuous isClosed_iInter TopologicalSpace.Closeds.isClosed' Scheme.IdealSheafData.support_iSup Scheme.IdealSheafData.support_comap
exists_mem_of_isClosed_of_nonempty' 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsClosed TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Set.Nonempty IsCompact Set.MapsTo DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Set Set.instMembership CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	exists_mem_of_isClosed_of_nonempty CategoryTheory.Over.initial_forget CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty CategoryTheory.IsCofiltered.over CategoryTheory.Over.w
exists_preimage_eq 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map IsCompact TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace CategoryTheory.Limits.Cone.pt SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe Scheme.Opens TopologicalSpace.Opens.instSetLike	Preorder.smallCategory TopologicalSpace.Opens TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact isBasis_preimage_isAffineOpen CategoryTheory.IsCofiltered.inf_objs_exists Preorder.subsingleton_hom Set.toFinite_toFinset isOpen_iUnion TopologicalSpace.Opens.is_open' isCompact_iUnion IsAffineOpen.isCompact IsAffineOpen.preimage Scheme.Hom.preimage_iSup CategoryTheory.Limits.Cone.w sSup_eq_iSup'
instIsAffineHomMapOverSchemeOpensDiagram 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map	CategoryTheory.Over CategoryTheory.instCategoryOver opensDiagram	—	Scheme.Opens.instIsOpenImmersionι TopologicalSpace.Opens.ext Set.ext CategoryTheory.Functor.map_comp CategoryTheory.Over.w Scheme.Hom.coe_resLE_apply IsAffineOpen.preimage_of_isOpenImmersion IsAffineOpen.preimage IsAffineOpen.image_of_isOpenImmersion Scheme.Opens.opensRange_ι Scheme.Hom.comp_apply
instIsOpenImmersionAppOverSchemeOpensDiagramι 📖	mathematical	—	IsOpenImmersion CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory opensDiagram CategoryTheory.Functor.comp CategoryTheory.Over.forget CategoryTheory.NatTrans.app opensDiagramι	—	Scheme.Opens.instIsOpenImmersionι
instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace	CategoryTheory.Limits.PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp Scheme.Γ	—	nonempty_isColimit_Γ_mapCocone CategoryTheory.Limits.preservesLimit_rightOp
isAffineHom_π_app 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	IsAffineOpen.preimage Scheme.isAffine_of_isLimit
isBasis_preimage_isAffineOpen 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map	TopologicalSpace.Opens.IsBasis TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace CategoryTheory.Limits.Cone.pt SheafedSpace.instTopologicalSpaceCarrierCarrier setOf TopologicalSpace.Opens Scheme.Opens IsAffineOpen Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	TopologicalSpace.Opens.isBasis_iff_nbhd CategoryTheory.IsCofiltered.nonempty TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ IsAffineOpen.preimage IsAffineOpen.exists_basicOpen_le Scheme.isAffine_of_isLimit CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.comp_preservesColimit preservesColimit_Γ CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.IsCofiltered.over CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty RingEquiv.surjective CategoryTheory.Limits.Cone.w Eq.ge LE.le.trans Scheme.Opens.instIsOpenImmersionι Scheme.Hom.le_resLE_preimage_iff le_rfl CategoryTheory.eqToHom_op Scheme.Hom.app_eq_appLE Scheme.Hom.resLE_appLE Scheme.Hom.appLE_map Scheme.Hom.map_appLE RingEquiv.symm_apply_eq IsAffineOpen.basicOpen Scheme.preimage_basicOpen Scheme.basicOpen_res_eq CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom CommRingCat.comp_apply
nonempty_isColimit_Γ_mapCocone 📖	mathematical	IsAffineHom CategoryTheory.Functor.obj Scheme Scheme.instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace	CategoryTheory.Limits.IsColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op Scheme.Γ CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cone.op	—	CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms CommRingCat.forgetReflectIsos CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.Limits.ReflectsColimit.reflects CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.reflects_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty exists_appTop_π_eq_of_isLimit exists_app_map_eq_map_of_isLimit isCompact_univ
opensCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory opensDiagram opensCone Scheme.Opens.toScheme CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—
opensCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Scheme.Opens.toScheme CategoryTheory.Limits.Cone.pt Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Limits.Cone.π opensDiagram opensCone Scheme.Hom.resLE CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
opensDiagram_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory opensDiagram Scheme.Hom.resLE CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left Scheme.Opens CategoryTheory.Comma.right Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Comma.hom	—	—
opensDiagram_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory opensDiagram Scheme.Opens.toScheme CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Scheme.Opens CategoryTheory.Comma.right Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—
opensDiagramι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver Scheme Scheme.instCategory opensDiagram CategoryTheory.Functor.comp CategoryTheory.Over.forget opensDiagramι Scheme.Opens.ι CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Scheme.Opens CategoryTheory.Comma.right Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Functor.map CategoryTheory.Comma.hom	—	—

AlgebraicGeometry.ExistsHomHomCompEqCompAux

Definitions

Name	Category	Theorems
D' 📖	CompOp	—
a 📖	CompOp	4 math math: exists_eq, exists_index, ha, hab
b 📖	CompOp	4 math math: exists_eq, exists_index, hab, hb
c 📖	CompOp	1 math math: hab
c' 📖	CompOp	—
g 📖	CompOp	1 math math: range_g_subset
hc 📖	CompOp	—
hc' 📖	CompOp	—
hii' 📖	CompOp	1 math math: exists_eq
i 📖	CompOp	5 math math: exists_eq, exists_index, ha, hab, hb
i' 📖	CompOp	2 math math: exists_eq, range_g_subset
𝒰D 📖	CompOp	1 math math: exists_eq
𝒰D₀ 📖	CompOp	—
𝒰S 📖	CompOp	4 math math: h𝒰S, exists_index, h𝒰X, range_g_subset
𝒰X 📖	CompOp	3 math math: exists_index, h𝒰X, range_g_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq 📖	mathematical	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt c CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ i' AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange 𝒰D AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.PreZeroHypercover.f i hii' a b	—	AlgebraicGeometry.Scheme.isAffine_affineCover AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.locallyOfFiniteType_comp AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme CategoryTheory.Limits.pullback.condition AlgebraicGeometry.Scheme.local_affine CategoryTheory.Over.initial_forget CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty CategoryTheory.CreatesLimit.toReflectsLimit CategoryTheory.IsCofiltered.isConnected CategoryTheory.IsCofiltered.over CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Over.pullbackIsRightAdjoint CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace AlgebraicGeometry.Scheme.instIsQuasiAffineOfIsAffine h𝒰S h𝒰X CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.IsOpenImmersion.instFstScheme hab CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.limit.lift_π AlgebraicGeometry.Scheme.Pullback.diagonalCover_map AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition AlgebraicGeometry.isOpenImmersion_isStableUnderComposition CategoryTheory.Limits.Cone.w CategoryTheory.Limits.pullback.condition_assoc
exists_index 📖	mathematical	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.map	Set.preimage CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i CategoryTheory.Limits.pullback.lift a b Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app ha hb Compl.compl Set Set.instCompl SetLike.coe AlgebraicGeometry.Scheme.Opens CategoryTheory.Limits.pullback.diagonalObj TopologicalSpace.Opens.instSetLike AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange 𝒰S 𝒰X Set.instEmptyCollection	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback ha hb IsClosed.preimage AlgebraicGeometry.Scheme.Hom.continuous IsOpen.isClosed_compl TopologicalSpace.Opens.isOpen AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty' CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty IsClosed.isCompact CategoryTheory.Functor.map_comp AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Category.comp_id hab CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullback.diagonal_snd CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
ha 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const i CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct a	—	—
hab 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt c i CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π a b	—	—
hb 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const i CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct b	—	—
h𝒰S 📖	mathematical	—	AlgebraicGeometry.IsAffine CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion 𝒰S	—	—
h𝒰X 📖	mathematical	—	AlgebraicGeometry.IsAffine CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange 𝒰S AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.PreZeroHypercover.f 𝒰X	—	—
range_g_subset 📖	mathematical	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.map	Set CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback Set.instHasSubset Set.range i' DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' g SetLike.coe AlgebraicGeometry.Scheme.Opens CategoryTheory.Limits.pullback.diagonalObj TopologicalSpace.Opens.instSetLike AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange 𝒰S 𝒰X	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback exists_index ha hb

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_of_isLimit 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.Limits.Cone.pt	—	CategoryTheory.IsCofiltered.nonempty AlgebraicGeometry.isAffineHom_π_app AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace AlgebraicGeometry.instQuasiCompactOfIsAffineHom
exists_hom_comp_eq_comp_of_locallyOfFiniteType 📖	—	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.Cone.π	—	—	AlgebraicGeometry.isAffineHom_π_app isAffine_affineCover instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange Pullback.instHasPullback isEmpty_or_nonempty CategoryTheory.Limits.IsInitial.hom_ext instJointlySurjectivePrecoverage Cover.nonempty_of_nonempty CategoryTheory.IsCofiltered.inf_exists Finset.mem_image_of_mem Finset.mem_univ Cover.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc Mathlib.Tactic.Reassoc.eq_whisker' AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq
exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType 📖	—	CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.Cone.π	—	—	CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty exists_hom_comp_eq_comp_of_locallyOfFiniteType CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id CategoryTheory.Limits.Cone.w_assoc CategoryTheory.Functor.map_comp
exists_isAffine_of_isLimit 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace	AlgebraicGeometry.IsAffine	—	AlgebraicGeometry.isAffineHom_π_app exists_isQuasiAffine_of_isLimit instIsQuasiAffineOfIsAffine AlgebraicGeometry.isAffineHom_of_isAffine AlgebraicGeometry.isAffine_Spec IsQuasiAffine.toCompactSpace instIsOpenImmersionToSpecΓOfIsQuasiAffine AlgebraicGeometry.exists_map_eq_top CategoryTheory.Limits.comp_preservesLimit AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint preimage_opensRange_toSpecΓ Hom.opensRange_of_isIso AlgebraicGeometry.IsAffine.affine IsQuasiAffine.of_isAffineHom AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top
exists_isOpenCover_and_isAffine 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace TopologicalSpace.IsOpenCover CategoryTheory.Limits.Cone.pt AlgebraicGeometry.IsAffineOpen	Finset SetLike.instMembership Finset.instSetLike Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	compactSpace_of_isLimit IsCompact.elim_finite_subcover isCompact_univ TopologicalSpace.Opens.isOpen Eq.ge TopologicalSpace.IsOpenCover.iSup_set_eq_univ CategoryTheory.IsCofiltered.inf_objs_exists Finset.mem_image_of_mem AlgebraicGeometry.exists_map_eq_top Hom.preimage_iSup iSup_congr_Prop CategoryTheory.Limits.Cone.w top_le_iff isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop Set.mem_univ Eq.trans_le iSup_subtype CategoryTheory.Functor.map_comp AlgebraicGeometry.IsAffineOpen.preimage Hom.comp_preimage AlgebraicGeometry.exists_isAffineOpen_preimage_eq
exists_isQuasiAffine_of_isLimit 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace	IsQuasiAffine	—	CategoryTheory.IsCofiltered.nonempty TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isBasis_affineOpens Set.mem_univ isOpen_univ IsQuasiAffine.isBasis_basicOpen TopologicalSpace.Opens.isOpen AlgebraicGeometry.exists_appTop_π_eq_of_isLimit CategoryTheory.IsCofilteredOrEmpty.cone_objs CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty AlgebraicGeometry.exists_map_preimage_le_map_preimage AlgebraicGeometry.isCompact_basicOpen isCompact_univ preimage_basicOpen_top Hom.comp_preimage CategoryTheory.Limits.Cone.w le_top basicOpen_res inf_eq_right CategoryTheory.Functor.map_comp CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise Hom.comp_appTop AlgebraicGeometry.IsAffineOpen.basicOpen AlgebraicGeometry.IsAffineOpen.preimage CompactSpace.elim_nhds_subcover IsQuasiAffine.toCompactSpace IsOpen.mem_nhds TopologicalSpace.Opens.is_open' CategoryTheory.IsCofiltered.inf_objs_exists Finset.mem_image_of_mem AlgebraicGeometry.exists_map_eq_top top_le_iff TopologicalSpace.Opens.mem_iSup IsQuasiAffine.of_forall_exists_mem_basicOpen Eq.ge Set.mem_iUnion₂
exists_π_app_comp_eq_of_locallyOfFinitePresentation 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map CompactSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier QuasiSeparatedSpace CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.Cone.π	CategoryTheory.NatTrans.app	—	TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le isBasis_affineOpens TopologicalSpace.IsOpenCover.comap TopologicalSpace.Opens.IsBasis.isOpenCover exists_isOpenCover_and_isAffine CategoryTheory.IsCofiltered.wideCospan CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty Finite.of_fintype CategoryTheory.Functor.map_comp Hom.comp_preimage LE.le.trans Hom.preimage_mono CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id AlgebraicGeometry.exists_map_preimage_le_map_preimage AlgebraicGeometry.IsAffineOpen.isCompact CategoryTheory.NatTrans.comp_app Eq.trans_le Subtype.prop CategoryTheory.Limits.Cone.w AlgebraicGeometry.IsAffineOpen.preimage Hom.resLE_comp_resLE Hom.resLE.congr_simp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' le_refl Hom.resLE_comp_ι AlgebraicGeometry.morphismRestrict_ι_assoc homOfLE_ι_assoc le_rfl Hom.map_resLE_assoc Hom.resLE_comp_resLE_assoc CategoryTheory.IsCofiltered.over AlgebraicGeometry.instLocallyOfFinitePresentationResLE AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens CategoryTheory.NatTrans.ext' inf_le_left inf_le_right isCompact_iff_compactSpace AlgebraicGeometry.QuasiCompact.isCompact_preimage AlgebraicGeometry.instQuasiCompactOfIsAffineHom TopologicalSpace.Opens.isOpen IsCompact.inter_of_isOpen TopologicalSpace.Opens.is_open' CategoryTheory.Functor.map_id TopologicalSpace.Opens.map_id_obj exists_hom_comp_eq_comp_of_locallyOfFiniteType AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation AlgebraicGeometry.instIsAffineHomMapOverSchemeOpensDiagram Hom.resLE_map_assoc CategoryTheory.Discrete.functor_map_id Finite.instProd AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionF Pullback.instHasPullback AlgebraicGeometry.isPullback_opens_inf CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.IsPullback.isoPullback_hom_fst_assoc CategoryTheory.IsPullback.isoPullback_hom_snd_assoc Cover.ι_glueMorphisms Cover.hom_ext instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.IsPullback.flip AlgebraicGeometry.isPullback_morphismRestrict CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Limits.Cone.w_assoc Cover.ι_glueMorphisms_assoc
nonempty_of_isLimit 📖	mathematical	AlgebraicGeometry.IsAffineHom CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.Functor.map TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CompactSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.Limits.Cone.pt	—	isEmpty_or_nonempty Nonempty.map AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier ULift.nontrivial Int.instNontrivial local_affine instJointlySurjectivePrecoverage AlgebraicGeometry.isAffine_Spec instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange Pullback.instHasPullback CategoryTheory.Functor.map_comp CategoryTheory.IsCofiltered.infTo_commutes Finset.mem_image_of_mem Finset.mem_univ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp Function.isEmpty Cover.covers Mathlib.Tactic.Push.not_forall_eq CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.isAffineHom_isStableUnderBaseChange AlgebraicGeometry.isAffine_of_isAffineHom AlgebraicGeometry.IsAffine.affine CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_hasLimitsOfSize CategoryTheory.Limits.hasLimits_op_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsCofiltered.over CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint PrimeSpectrum.instNonemptyOfNontrivial component_nontrivial CommRingCat.FilteredColimits.nontrivial CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty CategoryTheory.Over.initial_forget

---

← Back to Index