Limits

📁 Source: Mathlib/AlgebraicGeometry/Limits.lean

Statistics

Metric	Count
Definitions `coprodPresheafObjIso`, `emptyTo`, `hom_unique_of_empty_source`, `coprodIsoSigma`, `coprodMk`, `coprodOpenCover`, `coprodSpec`, `emptyIsInitial`, `instBraidedCategoryScheme`, `instCartesianMonoidalCategoryScheme`, `instCreatesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpaceOfSmall`, `instOverTerminalScheme`, `isInitialOfIsEmpty`, `sigmaMk`, `sigmaOpenCover`, `sigmaSpec`, `specPUnitIsInitial`, `specPunitIsInitial`, `specULiftZIsTerminal`, `specZIsTerminal`	20
Theorems `biSup_of_disjoint`, `iSup_of_disjoint`, `of_subsingleton`, `sup_of_disjoint`, `coprodPresheafObjIso_hom_fst`, `coprodPresheafObjIso_hom_fst_assoc`, `coprodPresheafObjIso_hom_snd`, `coprodPresheafObjIso_hom_snd_assoc`, `emptyTo_base`, `emptyTo_c_app`, `empty_ext`, `empty_ext_iff`, `eq_emptyTo`, `isAffine_of_isLimit`, `coprodMk_inl`, `coprodMk_inr`, `coprodSpec_apply`, `coprodSpec_coprodMk`, `coprodSpec_inl`, `coprodSpec_inl_assoc`, `coprodSpec_inr`, `coprodSpec_inr_assoc`, `disjoint_opensRange_sigmaι`, `emptyIsInitial_to`, `initial_isEmpty`, `inl_ne_inr`, `inr_ne_inl`, `instCoproductsOfShapeDisjointSchemeOfSmall`, `instFinitaryExtensiveScheme`, `instHasColimitsOfShapeDiscreteSchemeOfSmall`, `instHasFiniteCoproductsScheme`, `instHasFiniteLimitsScheme`, `instHasInitialScheme`, `instHasStrictInitialObjectsScheme`, `instHasTerminalScheme`, `instIsAffineCoprodScheme`, `instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat`, `instIsAffineOfSubsingletonCarrierCarrierCommRingCat`, `instIsAffineSigmaObjScheme`, `instIsAffineTerminalScheme`, `instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme`, `instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec`, `instIsIsoSchemeCoprodSpec`, `instIsIsoSchemeSigmaSpecOfFinite`, `instIsOpenImmersionInlScheme`, `instIsOpenImmersionInrScheme`, `instIsOpenImmersionMapOfHomForallEvalRingHom`, `instIsOpenImmersionMapWalkingSpanSchemeSpan`, `instIsOpenImmersionSigmaSpec`, `instIsOverTerminalScheme`, `instMonoCoprodScheme`, `instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion`, `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec`, `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite`, `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec`, `instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall`, `instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty`, `instSubsingletonOverTerminalScheme`, `isAffineOpen_bot`, `isAffine_of_isEmpty`, `isCompl_opensRange_inl_inr`, `isCompl_range_inl_inr`, `isEmpty_of_commSq_sigmaι_of_ne`, `isEmpty_pullback_sigmaι_of_ne`, `isInitial_iff_isEmpty`, `isIso_of_isEmpty`, `isIso_stalkMap_coprodSpec`, `isOpenImmersion_of_isEmpty`, `isOpenImmersion_sigmaDesc`, `isPullback_inl_inl_coprodMap`, `isPullback_inr_inr_coprodMap`, `nonempty_isColimit_binaryCofanMk_of_isCompl`, `nonempty_isColimit_cofanMk_of`, `sigmaMk_mk`, `sigmaOpenCover_I₀`, `sigmaOpenCover_X`, `sigmaOpenCover_f`, `sigmaι_eq_iff`, `spec_punit_isEmpty`, `ι_left_coprodIsoSigma_inv`, `ι_right_coprodIsoSigma_inv`, `ι_sigmaSpec`, `ι_sigmaSpec_assoc`	83
Total	103

AlgebraicGeometry

Definitions

Name	Category	Theorems
`coprodIsoSigma` 📖	CompOp	2 math math: `ι_right_coprodIsoSigma_inv`, `ι_left_coprodIsoSigma_inv`
`coprodMk` 📖	CompOp	4 math math: `coprodSpec_apply`, `coprodMk_inl`, `coprodSpec_coprodMk`, `coprodMk_inr`
`coprodOpenCover` 📖	CompOp	—
`coprodSpec` 📖	CompOp	8 math math: `coprodSpec_apply`, `coprodSpec_inr`, `isIso_stalkMap_coprodSpec`, `coprodSpec_coprodMk`, `coprodSpec_inr_assoc`, `coprodSpec_inl_assoc`, `coprodSpec_inl`, `instIsIsoSchemeCoprodSpec`
`emptyIsInitial` 📖	CompOp	1 math math: `emptyIsInitial_to`
`instBraidedCategoryScheme` 📖	CompOp	—
`instCartesianMonoidalCategoryScheme` 📖	CompOp	5 math math: `instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat`, `Scheme.isSeparated_iff_isClosedImmersion_prod_lift`, `IsImmersion.instLiftSchemeId`, `Scheme.instIsClosedImmersionLiftIdOfIsSeparated`, `quasiSeparatedSpace_iff_quasiCompact_prod_lift`
`instCreatesColimitsOfShapeSchemeLocallyRingedSpaceDiscreteForgetToLocallyRingedSpaceOfSmall` 📖	CompOp	—
`instOverTerminalScheme` 📖	CompOp	—
`isInitialOfIsEmpty` 📖	CompOp	—
`sigmaMk` 📖	CompOp	1 math math: `sigmaMk_mk`
`sigmaOpenCover` 📖	CompOp	3 math math: `sigmaOpenCover_X`, `sigmaOpenCover_I₀`, `sigmaOpenCover_f`
`sigmaSpec` 📖	CompOp	4 math math: `ι_sigmaSpec`, `instIsIsoSchemeSigmaSpecOfFinite`, `instIsOpenImmersionSigmaSpec`, `ι_sigmaSpec_assoc`
`specPUnitIsInitial` 📖	CompOp	—
`specPunitIsInitial` 📖	CompOp	—
`specULiftZIsTerminal` 📖	CompOp	—
`specZIsTerminal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprodMk_inl` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instTopologicalSpaceSum` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `coprodMk` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inl`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.FinitaryExtensive.hasFiniteCoproducts` `CategoryTheory.finitaryExtensive_TopCat` `Finite.of_fintype` `CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc` `CategoryTheory.Limits.coprodComparison_inl`
`coprodMk_inr` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instTopologicalSpaceSum` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `coprodMk` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inr`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.FinitaryExtensive.hasFiniteCoproducts` `CategoryTheory.finitaryExtensive_TopCat` `Finite.of_fintype` `CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc` `CategoryTheory.Limits.coprodComparison_inr`
`coprodSpec_apply` 📖	mathematical	—	`DFunLike.coe` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Spec` `CommRingCat.of` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Prod.instCommRing` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `coprodSpec` `Equiv` `PrimeSpectrum` `CommRing.toCommSemiring` `Prod.instCommSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `PrimeSpectrum.primeSpectrumProd` `Homeomorph` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `instTopologicalSpaceSum` `Homeomorph.instEquivLike` `Homeomorph.symm` `coprodMk`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `coprodSpec_coprodMk` `Homeomorph.apply_symm_apply`
`coprodSpec_coprodMk` 📖	mathematical	—	`DFunLike.coe` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Spec` `CommRingCat.of` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Prod.instCommRing` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `coprodSpec` `Homeomorph` `instTopologicalSpaceSum` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `coprodMk` `Equiv` `PrimeSpectrum` `CommRing.toCommSemiring` `Prod.instCommSemiring` `Equiv.instEquivLike` `Equiv.symm` `PrimeSpectrum.primeSpectrumProd`	—	`PrimeSpectrum.ext` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `coprodMk_inl` `CategoryTheory.Limits.coprod.inl_desc` `Ideal.ext` `RingHom.instRingHomClass` `Ideal.comap_top` `inf_of_le_left` `coprodMk_inr` `CategoryTheory.Limits.coprod.inr_desc` `inf_of_le_right`
`coprodSpec_inl` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Prod.instCommRing` `CategoryTheory.Limits.coprod.inl` `coprodSpec` `Spec.map` `CommRingCat.ofHom` `RingHom.fst` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`CategoryTheory.Limits.coprod.inl_desc` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`coprodSpec_inl_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inl` `Prod.instCommRing` `coprodSpec` `Spec.map` `CommRingCat.ofHom` `RingHom.fst` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `coprodSpec_inl`
`coprodSpec_inr` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Prod.instCommRing` `CategoryTheory.Limits.coprod.inr` `coprodSpec` `Spec.map` `CommRingCat.ofHom` `RingHom.snd` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`CategoryTheory.Limits.coprod.inr_desc` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`coprodSpec_inr_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inr` `Prod.instCommRing` `coprodSpec` `Spec.map` `CommRingCat.ofHom` `RingHom.snd` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `coprodSpec_inr`
`disjoint_opensRange_sigmaι` 📖	mathematical	—	`Disjoint` `Scheme.Opens` `CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame` `Scheme.Hom.opensRange` `CategoryTheory.Limits.Sigma.ι` `Scheme.IsLocallyDirected.instIsOpenImmersionι`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `sigmaι_eq_iff`
`emptyIsInitial_to` 📖	mathematical	—	`CategoryTheory.Limits.IsInitial.to` `Scheme` `Scheme.instCategory` `Scheme.instEmptyCollection` `emptyIsInitial` `Scheme.emptyTo`	—	—
`initial_isEmpty` 📖	mathematical	—	`IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.initial` `Scheme` `Scheme.instCategory` `instHasInitialScheme`	—	`instHasInitialScheme`
`inl_ne_inr` 📖	—	—	—	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set.disjoint_iff_forall_ne` `IsCompl.disjoint` `isCompl_range_inl_inr`
`inr_ne_inl` 📖	—	—	—	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `inl_ne_inr`
`instCoproductsOfShapeDisjointSchemeOfSmall` 📖	mathematical	—	`CategoryTheory.Limits.CoproductsOfShapeDisjoint` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `IsOpenImmersion.mono` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `Scheme.Pullback.instHasPullback` `isInitial_iff_isEmpty` `isEmpty_pullback_sigmaι_of_ne`
`instFinitaryExtensiveScheme` 📖	mathematical	—	`CategoryTheory.FinitaryExtensive` `Scheme` `Scheme.instCategory`	—	`instHasColimitsOfShapeDiscreteSchemeOfSmall` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `Finite.of_fintype` `Scheme.Pullback.instHasPullbacks` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.IsPullback.flip` `IsOpenImmersion.isPullback` `instIsOpenImmersionInlScheme` `TopologicalSpace.Opens.ext` `Set.ext` `Homeomorph.surjective` `coprodMk_inl` `coprodMk_inr` `instIsOpenImmersionInrScheme` `nonempty_isColimit_binaryCofanMk_of_isCompl` `IsOpenImmersion.instFstScheme` `IsOpenImmersion.hasPullback_of_right` `Scheme.Hom.opensRange_pullbackFst` `IsCompl.map` `CoheytingHomClass.toBoundedLatticeHomClass` `BiheytingHomClass.toCoheytingHomClass` `BoundedLatticeHomClass.toBiheytingHomClass` `CompleteLatticeHomClass.toBoundedLatticeHomClass` `CompleteLatticeHom.instCompleteLatticeHomClass` `isCompl_range_inl_inr` `CategoryTheory.IsVanKampenColimit.of_iso`
`instHasColimitsOfShapeDiscreteSchemeOfSmall` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.hasColimit_of_created` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace`
`instHasFiniteCoproductsScheme` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteCoproducts` `Scheme` `Scheme.instCategory`	—	`instHasColimitsOfShapeDiscreteSchemeOfSmall` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`instHasFiniteLimitsScheme` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks` `instHasTerminalScheme` `Scheme.Pullback.instHasPullbacks`
`instHasInitialScheme` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.hasInitial_of_unique` `Unique.instSubsingleton`
`instHasStrictInitialObjectsScheme` 📖	mathematical	—	`CategoryTheory.Limits.HasStrictInitialObjects` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict` `instHasInitialScheme` `isIso_of_isEmpty` `initial_isEmpty`
`instHasTerminalScheme` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit` `CategoryTheory.Limits.hasTerminal_op_of_hasInitial` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `Finite.of_fintype` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint`
`instIsAffineCoprodScheme` 📖	mathematical	—	`IsAffine` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self`	—	`IsAffine.of_isIso` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `instIsIsoSchemeCoprodSpec` `isAffine_Spec`
`instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat` 📖	mathematical	—	`IsAffine`	—	`isOpen_discrete` `IsAffineOpen.iSup_of_disjoint` `IsAffineOpen.of_subsingleton` `Set.subsingleton_singleton` `TopologicalSpace.Opens.ext` `Set.ext` `isOpen_iUnion` `IsAffine.of_isIso` `CategoryTheory.Iso.isIso_inv`
`instIsAffineOfSubsingletonCarrierCarrierCommRingCat` 📖	mathematical	—	`IsAffine`	—	`isEmpty_or_nonempty` `isAffine_of_isEmpty` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `Scheme.isBasis_affineOpens` `isOpen_univ` `IsAffine.of_isIso` `CategoryTheory.Iso.isIso_inv` `TopologicalSpace.Opens.ext` `Set.ext`
`instIsAffineSigmaObjScheme` 📖	mathematical	`IsAffine`	`CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Countable.toSmall` `Finite.to_countable`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Countable.toSmall` `Finite.to_countable` `Small.equiv_small` `Equiv.finite_iff` `IsAffine.of_isIso` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeDiscreteSchemeOfSmall` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Iso.isIso_hom` `instIsIsoSchemeSigmaSpecOfFinite` `isAffine_Spec`
`instIsAffineTerminalScheme` 📖	mathematical	—	`IsAffine` `CategoryTheory.Limits.terminal` `Scheme` `Scheme.instCategory` `instHasTerminalScheme`	—	`IsAffine.of_isIso` `instHasTerminalScheme` `CategoryTheory.Limits.hasTerminal_op_of_hasInitial` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `Finite.of_fintype` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint` `CategoryTheory.Iso.isIso_inv` `instIsAffineObjOppositeCommRingCatSchemeSpec`
`instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme` 📖	mathematical	—	`IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme` `Scheme.instEmptyCollection`	—	`PEmpty.instIsEmpty`
`instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.coprod` `CategoryTheory.Functor.obj` `Opposite` `CommRingCat` `CategoryTheory.Category.opposite` `CommRingCat.instCategory` `Scheme.Spec` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasCoproducts_opposite` `CommRingCat.hasLimitsOfShape` `CategoryTheory.Limits.coprodComparison`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasCoproducts_opposite` `CommRingCat.hasLimitsOfShape` `CategoryTheory.Limits.instHasBinaryCoproductOppositeOp` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Limits.coprod.hom_ext` `CategoryTheory.Limits.coprodComparison_inl_assoc` `coprodSpec.eq_1` `CategoryTheory.Limits.coprod.inl_desc` `Scheme.Spec_map` `Spec.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.unop_inv` `CategoryTheory.Limits.opProdIsoCoprod_inv_inl` `CategoryTheory.Limits.limit.isoLimitCone_inv_π` `CategoryTheory.Limits.coprodComparison_inr_assoc` `CategoryTheory.Limits.coprod.inr_desc` `CategoryTheory.Limits.opProdIsoCoprod_inv_inr` `instIsIsoSchemeMapOfCommRingCat` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsIso.eq_comp_inv` `instIsIsoSchemeCoprodSpec` `CategoryTheory.IsIso.inv_isIso`
`instIsIsoSchemeCoprodSpec` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.coprod` `Spec` `CommRingCat.of` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Prod.instCommRing` `coprodSpec`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.Colimits.hasColimits_commRingCat` `isIso_iff_isIso_stalkMap` `TopCat.ext` `coprodSpec_apply` `CategoryTheory.Iso.isIso_inv` `isIso_stalkMap_coprodSpec`
`instIsIsoSchemeSigmaSpecOfFinite` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Spec` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `sigmaSpec`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite` `CategoryTheory.Limits.Sigma.hom_ext` `ι_sigmaSpec` `CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.isIso_hom`
`instIsOpenImmersionInlScheme` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inl`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `small_ulift` `ι_left_coprodIsoSigma_inv` `IsOpenImmersion.comp` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `CategoryTheory.Iso.isIso_inv`
`instIsOpenImmersionInrScheme` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inr`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `small_ulift` `ι_right_coprodIsoSigma_inv` `IsOpenImmersion.comp` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `CategoryTheory.Iso.isIso_inv`
`instIsOpenImmersionMapOfHomForallEvalRingHom` 📖	mathematical	—	`IsOpenImmersion` `Spec` `CommRingCat.of` `Pi.commRing` `Spec.map` `CommRingCat.ofHom` `Pi.evalRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsLocalization.away_of_isIdempotentElem_of_mul` `Function.update_self` `mul_one` `Function.update_of_ne` `MulZeroClass.mul_zero` `one_mul` `MulZeroClass.zero_mul` `Function.surjective_eval` `AddTorsor.nonempty` `IsOpenImmersion.of_isLocalization`
`instIsOpenImmersionMapWalkingSpanSchemeSpan` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.span` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_id` `IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id`
`instIsOpenImmersionSigmaSpec` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Spec` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `sigmaSpec`	—	`isOpenImmersion_sigmaDesc` `UnivLE.small` `UnivLE.self` `instIsOpenImmersionMapOfHomForallEvalRingHom` `Set.disjoint_iff_forall_ne` `Eq.le` `PrimeSpectrum.ext_iff` `DFinsupp.single_apply` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Ideal.IsPrime.ne_top` `PrimeSpectrum.isPrime`
`instIsOverTerminalScheme` 📖	mathematical	—	`Scheme.Hom.IsOver` `CategoryTheory.Limits.terminal` `Scheme` `Scheme.instCategory` `instHasTerminalScheme`	—	`instHasTerminalScheme` `Unique.instSubsingleton`
`instMonoCoprodScheme` 📖	mathematical	—	`CategoryTheory.Limits.MonoCoprod` `Scheme` `Scheme.instCategory`	—	`CategoryTheory.Limits.MonoCoprod.mk'` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `IsOpenImmersion.mono` `Scheme.IsLocallyDirected.instIsOpenImmersionι`
`instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Functor.comp` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.span` `Scheme.forget` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WidePushoutShape.Hom.init`	—	`CategoryTheory.mono_iff_injective` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `Scheme.Hom.isOpenEmbedding`
`instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Opposite` `CommRingCat` `CategoryTheory.Category.opposite` `CommRingCat.instCategory` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Scheme.Spec`	—	`CategoryTheory.Limits.hasInitial_op_of_hasTerminal` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CommRingCat.hasLimits` `Finite.of_fintype` `Function.isEmpty` `spec_punit_isEmpty` `CategoryTheory.Limits.preservesInitial_of_iso` `instHasInitialScheme` `isIso_of_isEmpty` `CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial`
`instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Opposite` `CommRingCat` `CategoryTheory.Category.opposite` `CommRingCat.instCategory` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Scheme.Spec`	—	`CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial` `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec` `instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscretePEmptySpec` `CategoryTheory.Limits.hasFiniteCoproducts_opposite` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CommRingCat.hasLimits`
`instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteWalkingPairSpec` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Opposite` `CommRingCat` `CategoryTheory.Category.opposite` `CommRingCat.instCategory` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `Scheme.Spec`	—	`CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasCoproducts_opposite` `CommRingCat.hasLimitsOfShape` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec` `CategoryTheory.Limits.preservesColimit_of_iso_diagram`
`instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Scheme` `Scheme.instCategory` `TopCat` `TopCat.instCategory` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Scheme.forgetToTop`	—	`CategoryTheory.Limits.comp_preservesColimitsOfShape` `CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape` `LocallyRingedSpace.instHasColimitsOfShapeDiscrete` `LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace` `SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite` `CategoryTheory.instSmallDiscrete` `CommRingCat.hasLimitsOfShape` `Opposite.small`
`instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty` 📖	mathematical	—	`CommRingCat.carrier` `CategoryTheory.Functor.obj` `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`	—	`Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot` `Unique.instSubsingleton`
`instSubsingletonOverTerminalScheme` 📖	mathematical	—	`Scheme.Over` `CategoryTheory.Limits.terminal` `Scheme` `Scheme.instCategory` `instHasTerminalScheme`	—	`instHasTerminalScheme` `Unique.instSubsingleton`
`isAffineOpen_bot` 📖	mathematical	—	`IsAffineOpen` `Bot.bot` `Scheme.Opens` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `HeytingAlgebra.toOrderBot`	—	`isAffine_of_isEmpty` `Set.instIsEmptyElemEmptyCollection`
`isAffine_of_isEmpty` 📖	mathematical	—	`IsAffine`	—	`IsAffine.of_isIso` `isIso_of_isEmpty` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.inv_isIso` `spec_punit_isEmpty` `isAffine_Spec`
`isCompl_opensRange_inl_inr` 📖	mathematical	—	`IsCompl` `Scheme.Opens` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CompleteLattice.toBoundedOrder` `TopologicalSpace.Opens.instCompleteLattice` `Scheme.Hom.opensRange` `CategoryTheory.Limits.coprod.inl` `instIsOpenImmersionInlScheme` `CategoryTheory.Limits.coprod.inr` `instIsOpenImmersionInrScheme`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instIsOpenImmersionInlScheme` `instIsOpenImmersionInrScheme` `isCompl_range_inl_inr`
`isCompl_range_inl_inr` 📖	mathematical	—	`IsCompl` `Set` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder` `Set.range` `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.Limits.coprod.inl` `CategoryTheory.Limits.coprod.inr`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.binaryCofan_isColimit_iff` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall`
`isEmpty_of_commSq_sigmaι_of_ne` 📖	mathematical	`CategoryTheory.CommSq` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.Sigma.ι`	`IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `eq_bot_iff` `disjoint_iff` `disjoint_opensRange_sigmaι` `Scheme.Hom.comp_apply` `CategoryTheory.CommSq.w`
`isEmpty_pullback_sigmaι_of_ne` 📖	mathematical	—	`IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.Sigma.ι` `Scheme.Pullback.instHasPullback`	—	`isEmpty_of_commSq_sigmaι_of_ne` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.condition`
`isInitial_iff_isEmpty` 📖	mathematical	—	`CategoryTheory.Limits.IsInitial` `Scheme` `Scheme.instCategory` `IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace`	—	`Equiv.isEmpty` `CategoryTheory.Iso.isIso_hom` `spec_punit_isEmpty`
`isIso_of_isEmpty` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme` `Scheme.instCategory`	—	`TopCat.epi_iff_surjective` `IsOpenImmersion.isIso` `isOpenImmersion_of_isEmpty` `Function.isEmpty`
`isIso_stalkMap_coprodSpec` 📖	mathematical	—	`CategoryTheory.IsIso` `CommRingCat` `CommRingCat.instCategory` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `CommRingCat.of` `Prod.instCommRing` `PresheafedSpace.presheaf` `DFunLike.coe` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `coprodSpec` `Scheme.Hom.stalkMap`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.Colimits.hasColimits_commRingCat` `Homeomorph.surjective` `Scheme.Hom.stalkMap_comp` `coprodMk_inl` `Inseparable.of_eq` `coprodSpec_inl` `IsOpenImmersion.instIsIsoCommRingCatStalkMap` `instIsOpenImmersionInlScheme` `Scheme.Hom.stalkMap_congr_hom` `CategoryTheory.IsIso.comp_inv_eq` `IsOpenImmersion.of_isLocalization` `IsLocalization.away_fst` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsIso.inv_isIso` `coprodMk_inr` `coprodSpec_inr` `instIsOpenImmersionInrScheme` `IsLocalization.away_snd`
`isOpenImmersion_of_isEmpty` 📖	mathematical	—	`IsOpenImmersion`	—	`IsOpenImmersion.of_isIso_stalkMap` `Topology.IsOpenEmbedding.of_isEmpty` `CommRingCat.Colimits.hasColimits_commRingCat`
`isOpenImmersion_sigmaDesc` 📖	mathematical	`IsOpenImmersion` `Pairwise` `Function.onFun` `Set` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `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.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.Sigma.desc`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Small.equiv_small` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Sigma.hom_ext` `Equiv.surjective` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.Limits.Sigma.ι_reindex_inv_assoc` `IsOpenImmersion.comp` `CategoryTheory.Iso.isIso_inv` `Equiv.injective`
`isPullback_inl_inl_coprodMap` 📖	mathematical	—	`CategoryTheory.IsPullback` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inl` `CategoryTheory.Limits.coprod.map`	—	`IsOpenImmersion.isPullback` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instIsOpenImmersionInlScheme` `CategoryTheory.Limits.coprod.inl_map` `le_antisymm` `Homeomorph.surjective` `SetLike.mem_coe` `coprodMk_inl` `Set.disjoint_iff_forall_ne` `IsCompl.disjoint` `isCompl_range_inl_inr` `coprodMk_inr` `CategoryTheory.Limits.coprod.inr_map`
`isPullback_inr_inr_coprodMap` 📖	mathematical	—	`CategoryTheory.IsPullback` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.coprod` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.inr` `CategoryTheory.Limits.coprod.map`	—	`CategoryTheory.IsPullback.of_iso` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `isPullback_inl_inl_coprodMap` `instHasColimitsOfShapeDiscreteSchemeOfSmall` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.Limits.coprod.map_desc` `CategoryTheory.Limits.coprod.desc_comp` `CategoryTheory.Limits.coprod.inr_map` `CategoryTheory.Limits.coprod.inl_map`
`nonempty_isColimit_binaryCofanMk_of_isCompl` 📖	mathematical	`IsCompl` `Scheme.Opens` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CompleteLattice.toBoundedOrder` `TopologicalSpace.Opens.instCompleteLattice` `Scheme.Hom.opensRange`	`CategoryTheory.Limits.IsColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.pair`	—	`nonempty_isColimit_cofanMk_of` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Equiv.iSup_comp` `iSup_bool_eq` `IsCompl.codisjoint` `IsCompl.disjoint` `Disjoint.symm`
`nonempty_isColimit_cofanMk_of` 📖	mathematical	`IsOpenImmersion` `iSup` `Scheme.Opens` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Scheme.Hom.opensRange` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Pairwise` `Function.onFun` `Disjoint` `TopologicalSpace.Opens.instPartialOrder` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame`	`CategoryTheory.Limits.IsColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Scheme` `Scheme.instCategory` `CategoryTheory.Discrete.functor`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `isOpenImmersion_sigmaDesc` `CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc` `isIso_of_isOpenImmersion_of_opensRange_eq_top` `eq_top_iff` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `CategoryTheory.Limits.colimit.ι_desc`
`sigmaMk_mk` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `instTopologicalSpaceSigma` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `sigmaMk` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.Limits.Sigma.ι`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `TopCat.topCat_hasColimitsOfShape` `univLE_of_max` `CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc` `CategoryTheory.Limits.ι_comp_sigmaComparison`
`sigmaOpenCover_I₀` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.I₀` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion` `sigmaOpenCover`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete`
`sigmaOpenCover_X` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion` `sigmaOpenCover`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete`
`sigmaOpenCover_f` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.f` `Scheme` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion` `sigmaOpenCover` `CategoryTheory.Limits.Sigma.ι`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete`
`sigmaι_eq_iff` 📖	mathematical	—	`DFunLike.coe` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CategoryTheory.Limits.Sigma.ι`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `Scheme.IsLocallyDirected.ι_eq_ι_iff` `CategoryTheory.Discrete.functor_map_id`
`spec_punit_isEmpty` 📖	mathematical	—	`IsEmpty` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `CommRingCat.of` `PUnit.commRing`	—	`PrimeSpectrum.instIsEmptyOfSubsingleton`
`ι_left_coprodIsoSigma_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.WalkingPair.left` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `small_ulift` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.Sigma.ι` `CategoryTheory.Iso.inv` `coprodIsoSigma` `CategoryTheory.Limits.coprod.inl`	—	`CategoryTheory.Limits.Sigma.ι_comp_map'` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `small_ulift` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`ι_right_coprodIsoSigma_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.WalkingPair.right` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `small_ulift` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.Sigma.ι` `CategoryTheory.Iso.inv` `coprodIsoSigma` `CategoryTheory.Limits.coprod.inr`	—	`CategoryTheory.Limits.Sigma.ι_comp_map'` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `small_ulift` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`ι_sigmaSpec` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `CategoryTheory.Limits.Sigma.ι` `sigmaSpec` `Spec.map` `CommRingCat.ofHom` `Pi.evalRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`CategoryTheory.Limits.Sigma.ι_desc` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`ι_sigmaSpec_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CategoryTheory.Limits.sigmaObj` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.Sigma.ι` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `sigmaSpec` `Spec.map` `CommRingCat.ofHom` `Pi.evalRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_sigmaSpec`

AlgebraicGeometry.IsAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biSup_of_disjoint` 📖	mathematical	`AlgebraicGeometry.IsAffineOpen` `Set.Pairwise` `Function.onFun` `AlgebraicGeometry.Scheme.Opens` `Disjoint` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `Set` `Set.instMembership`	—	`iSup_subtype''` `Set.Finite.to_subtype` `iSup_of_disjoint`
`iSup_of_disjoint` 📖	mathematical	`AlgebraicGeometry.IsAffineOpen` `Pairwise` `Function.onFun` `AlgebraicGeometry.Scheme.Opens` `Disjoint` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	`Small.equiv_small` `Countable.toSmall` `Finite.to_countable` `Equiv.finite_iff` `Equiv.iSup_congr` `Equiv.injective`
`of_subsingleton` 📖	mathematical	`Set.Subsingleton` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	`AlgebraicGeometry.IsAffineOpen`	—	`Set.Subsingleton.coe_sort` `AlgebraicGeometry.instIsAffineOfSubsingletonCarrierCarrierCommRingCat`
`sup_of_disjoint` 📖	mathematical	`Disjoint` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `TopologicalSpace.Opens.instFrame`	`AlgebraicGeometry.IsAffineOpen` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	`TopologicalSpace.Opens.ext` `Set.ext` `TopologicalSpace.Opens.coe_iSup` `iSup_of_disjoint` `Finite.instSum` `Finite.of_fintype` `instIsEmptyFalse`

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`coprodPresheafObjIso` 📖	CompOp	4 math math: `coprodPresheafObjIso_hom_fst_assoc`, `coprodPresheafObjIso_hom_snd_assoc`, `coprodPresheafObjIso_hom_snd`, `coprodPresheafObjIso_hom_fst`
`emptyTo` 📖	CompOp	4 math math: `emptyTo_base`, `AlgebraicGeometry.emptyIsInitial_to`, `emptyTo_c_app`, `eq_emptyTo`
`hom_unique_of_empty_source` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprodPresheafObjIso_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `instCategory` `IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `CategoryTheory.Limits.prod` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inl` `CategoryTheory.Limits.coprod.inr` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.forget` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.Iso.hom` `coprodPresheafObjIso` `CategoryTheory.Limits.prod.fst` `Hom.app`	—	`IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `AlgebraicGeometry.instIsOpenImmersionInlScheme` `AlgebraicGeometry.instIsOpenImmersionInrScheme` `Hom.preimage_image_eq` `CategoryTheory.eqToHom_op` `Hom.appIso_hom` `CategoryTheory.Category.assoc` `LE.le.trans` `le_of_eq` `Opposite.op_injective` `CategoryTheory.Limits.prod.map_fst` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.eqToHom_unop` `CategoryTheory.subsingleton_of_unop` `Preorder.subsingleton_hom` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`coprodPresheafObjIso_hom_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `instCategory` `IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `CategoryTheory.Limits.prod` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inl` `CategoryTheory.Limits.coprod.inr` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.forget` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.Iso.hom` `coprodPresheafObjIso` `CategoryTheory.Limits.prod.fst` `Hom.app`	—	`IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `coprodPresheafObjIso_hom_fst`
`coprodPresheafObjIso_hom_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `instCategory` `IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `CategoryTheory.Limits.prod` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inl` `CategoryTheory.Limits.coprod.inr` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.forget` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.Iso.hom` `coprodPresheafObjIso` `CategoryTheory.Limits.prod.snd` `Hom.app`	—	`IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `AlgebraicGeometry.instIsOpenImmersionInlScheme` `AlgebraicGeometry.instIsOpenImmersionInrScheme` `Hom.preimage_image_eq` `CategoryTheory.eqToHom_op` `Hom.appIso_hom` `CategoryTheory.Category.assoc` `LE.le.trans` `le_of_eq` `Opposite.op_injective` `CategoryTheory.Limits.prod.map_snd` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.eqToHom_unop` `CategoryTheory.subsingleton_of_unop` `Preorder.subsingleton_hom` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`coprodPresheafObjIso_hom_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `instCategory` `IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `CategoryTheory.Limits.prod` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `CategoryTheory.Limits.coprod.inl` `CategoryTheory.Limits.coprod.inr` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.forget` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.Iso.hom` `coprodPresheafObjIso` `CategoryTheory.Limits.prod.snd` `Hom.app`	—	`IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CommRingCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `coprodPresheafObjIso_hom_snd`
`emptyTo_base` 📖	mathematical	—	`AlgebraicGeometry.PresheafedSpace.Hom.base` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `AlgebraicGeometry.Scheme` `instEmptyCollection` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `emptyTo` `TopCat.ofHom` `TopCat.carrier` `instTopologicalSpacePEmpty` `TopCat.str`	—	—
`emptyTo_c_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `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` `CategoryTheory.Functor.obj` `TopCat.Presheaf` `AlgebraicGeometry.Scheme` `instEmptyCollection` `TopCat.instCategoryPresheaf` `TopCat.Presheaf.pushforward` `TopCat.ofHom` `instTopologicalSpacePEmpty` `AlgebraicGeometry.PresheafedSpace.Hom.c` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `Hom.toLRSHom'` `emptyTo` `CategoryTheory.Limits.IsTerminal.from` `CommRingCat.of` `PUnit.commRing` `CommRingCat.punitIsTerminal`	—	—
`empty_ext` 📖	—	—	—	—	`Hom.ext'` `Unique.instSubsingleton`
`empty_ext_iff` 📖	—	—	—	—	`empty_ext`
`eq_emptyTo` 📖	mathematical	—	`emptyTo`	—	`empty_ext`
`isAffine_of_isLimit` 📖	mathematical	`AlgebraicGeometry.IsAffine` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme` `instCategory`	`CategoryTheory.Limits.Cone.pt`	—	`AlgebraicGeometry.IsAffine.affine` `CategoryTheory.NatIso.isIso_of_isIso_app` `CategoryTheory.Limits.comp_preservesLimit` `AlgebraicGeometry.preservesLimit_rightOp_Γ` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint` `CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint` `AlgebraicGeometry.IsAffine.of_isIso` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.isAffine_Spec`

---

← Back to Index