Affine

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Statistics

Metric	Count
Definitions `IsAffineHom`	1
Theorems `isAffine_preimage`, `isCompact_pullback_inf`, `preimage`, `affinePreimage`, `instHasAffinePropertyIsAffineHomIsAffine`, `instIsAffineHomCompScheme`, `instIsAffineHomDescScheme`, `instIsAffineHomOfIsIsoScheme`, `instIsAffineHomιBasicOpen`, `instIsAffinePullbackSchemeOfIsAffineHom`, `instIsAffinePullbackSchemeOfIsAffineHom_1`, `instIsMultiplicativeSchemeIsAffineHom`, `instQuasiCompactOfIsAffineHom`, `isAffineHom_iff`, `isAffineHom_isStableUnderBaseChange`, `isAffineHom_of_forall_exists_isAffineOpen`, `isAffineHom_of_isAffine`, `isAffineHom_of_isInducing`, `isAffineOpen_of_isAffineOpen_basicOpen`, `isAffine_of_isAffineHom`, `isAffine_of_isAffineOpen_basicOpen`, `isIso_morphismRestrict_iff_isIso_app`, `isRetrocompact_basicOpen`	23
Total	24

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsAffineHom` 📖	CompData	32 math math: `instHasAffinePropertyIsAffineHomIsAffine`, `instIsAffineHomOfIsIsoScheme`, `IsIntegralHom.iff_universallyClosed_and_isAffineHom`, `IsAffineHom.comp_iff`, `isAffineHom_of_isAffine`, `IsClosedImmersion.instIsAffineHom`, `IsFinite.iff_isProper_and_isAffineHom`, `instIsAffineHomDescScheme`, `HasAffineProperty.affineAnd_eq_of_propertyIsLocal`, `isAffineHom_of_forall_exists_isAffineOpen`, `isClosedImmersion_iff_isAffineHom`, `isAffineHom_isStableUnderBaseChange`, `isAffineHom_of_isInducing`, `isAffineHom_iff`, `AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass`, `targetAffineLocally_affineAnd_eq_affineLocally`, `HasAffineProperty.affineAnd_iff`, `IsIntegralHom.toIsAffineHom`, `isIntegralHom_iff`, `IsFinite.toIsAffineHom`, `instIsAffineHomCompScheme`, `targetAffineLocally_affineAnd_iff'`, `IsFinite.eq_isProper_inf_isAffineHom`, `targetAffineLocally_affineAnd_iff_affineLocally`, `instHasOfPostcompPropertySchemeIsAffineHomIsSeparated`, `isFinite_iff`, `HasAffineProperty.affineAnd_le_isAffineHom`, `instIsMultiplicativeSchemeIsAffineHom`, `IsAffineHom.of_comp`, `IsIntegralHom.eq_universallyClosed_inf_isAffineHom`, `instIsAffineHomιBasicOpen`, `Scheme.Hom.instIsAffineHomToNormalization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affinePreimage` 📖	mathematical	—	`IsAffineOpen` `CategoryTheory.Functor.obj` `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'`	—	`IsAffineOpen.preimage`
`instHasAffinePropertyIsAffineHomIsAffine` 📖	mathematical	—	`HasAffineProperty` `IsAffineHom` `IsAffine`	—	`IsAffine.of_isIso` `CategoryTheory.Iso.isIso_hom` `Scheme.preimage_basicOpen` `IsAffineOpen.basicOpen` `isAffineOpen_top` `isAffine_of_isAffineOpen_basicOpen` `Ideal.map_top` `RingHom.instRingHomClass` `Ideal.map_span` `CategoryTheory.MorphismProperty.ext`
`instIsAffineHomCompScheme` 📖	mathematical	—	`IsAffineHom` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`Scheme.Hom.comp_base` `TopologicalSpace.Opens.map_comp_obj` `IsAffineHom.isAffine_preimage`
`instIsAffineHomDescScheme` 📖	mathematical	—	`IsAffineHom` `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.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` `IsAffineOpen.preimage` `instIsOpenImmersionMapScheme` `Scheme.Opens.instIsOpenImmersionι` `le_antisymm` `Homeomorph.surjective` `coprodMk_inl` `CategoryTheory.Limits.colimit.ι_desc` `CategoryTheory.Limits.coprod.inl_map` `coprodMk_inr` `CategoryTheory.Limits.coprod.inr_map` `isAffineOpen_opensRange` `instIsAffineCoprodScheme`
`instIsAffineHomOfIsIsoScheme` 📖	mathematical	—	`IsAffineHom`	—	`IsAffineOpen.preimage_of_isIso`
`instIsAffineHomιBasicOpen` 📖	mathematical	—	`IsAffineHom` `Scheme.Opens.toScheme` `Scheme.basicOpen` `Top.top` `Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.Opens.ι`	—	`Scheme.Opens.instIsOpenImmersionι` `Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion` `le_top` `Scheme.basicOpen_res` `TopologicalSpace.Opens.ext` `Set.image_preimage_eq_inter_range` `Scheme.Opens.range_ι` `IsAffineOpen.basicOpen`
`instIsAffinePullbackSchemeOfIsAffineHom` 📖	mathematical	—	`IsAffine` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback`	—	`isAffine_of_isAffineHom` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `isAffineHom_isStableUnderBaseChange`
`instIsAffinePullbackSchemeOfIsAffineHom_1` 📖	mathematical	—	`IsAffine` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback`	—	`isAffine_of_isAffineHom` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.pullback_fst` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `isAffineHom_isStableUnderBaseChange`
`instIsMultiplicativeSchemeIsAffineHom` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `IsAffineHom`	—	`instIsAffineHomOfIsIsoScheme` `CategoryTheory.IsIso.id` `instIsAffineHomCompScheme`
`instQuasiCompactOfIsAffineHom` 📖	mathematical	—	`QuasiCompact`	—	`quasiCompact_iff_forall_isAffineOpen` `IsAffineOpen.isCompact` `IsAffineOpen.preimage`
`isAffineHom_iff` 📖	mathematical	—	`IsAffineHom` `IsAffineOpen` `CategoryTheory.Functor.obj` `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'`	—	—
`isAffineHom_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `IsAffineHom`	—	`HasAffineProperty.isStableUnderBaseChange` `instHasAffinePropertyIsAffineHomIsAffine` `AffineTargetMorphismProperty.IsLocal.respectsIso` `HasAffineProperty.isLocal_affineProperty` `Scheme.Pullback.instHasPullback` `Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine`
`isAffineHom_of_forall_exists_isAffineOpen` 📖	mathematical	`TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `IsAffineOpen` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`IsAffineHom`	—	`HasAffineProperty.iff_of_iSup_eq_top` `instHasAffinePropertyIsAffineHomIsAffine` `top_le_iff`
`isAffineHom_of_isAffine` 📖	mathematical	—	`IsAffineHom`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyIsAffineHomIsAffine`
`isAffineHom_of_isInducing` 📖	mathematical	`Topology.IsInducing` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`IsAffineHom`	—	`isAffineHom_of_forall_exists_isAffineOpen` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `TopologicalSpace.Opens.isOpen` `Topology.IsInducing.isOpen_iff` `TopologicalSpace.Opens.is_open'` `inf_le_right` `TopologicalSpace.Opens.ext` `IsAffineOpen.exists_basicOpen_le` `IsAffineOpen.basicOpen` `Scheme.preimage_basicOpen` `Scheme.Hom.naturality` `Scheme.basicOpen_res` `IsClosed.isOpen_compl` `Set.preimage_eq_empty_iff` `Set.subset_compl_iff_disjoint_right` `isAffineOpen_bot`
`isAffineOpen_of_isAffineOpen_basicOpen` 📖	—	`Ideal.span` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsAffineOpen` `Scheme.basicOpen`	—	—	`isAffine_of_isAffineOpen_basicOpen` `Ideal.map_span` `RingHom.instRingHomClass` `Ideal.map_top` `Scheme.Opens.instIsOpenImmersionι` `Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion` `Scheme.image_basicOpen` `Scheme.Opens.ι_appIso` `CategoryTheory.eqToHom_op` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `Scheme.basicOpen_res_eq` `CategoryTheory.instIsIsoEqToHom`
`isAffine_of_isAffineHom` 📖	mathematical	—	`IsAffine`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyIsAffineHomIsAffine`
`isAffine_of_isAffineOpen_basicOpen` 📖	mathematical	`Ideal.span` `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` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsAffineOpen` `Scheme.basicOpen`	`IsAffine`	—	`Ideal.span_eq_top_iff_finite` `isCompact_univ_iff` `TopologicalSpace.Opens.coe_top` `iSup_basicOpen_of_span_eq_top` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `Set.iUnion_congr_Prop` `iSup_congr_Prop` `Finset.isCompact_biUnion` `IsAffineOpen.isCompact` `HasAffineProperty.of_iSup_eq_top` `instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop` `IsAffineOpen.basicOpen` `isAffineOpen_top` `instIsAffineObjOppositeCommRingCatSchemeSpec` `PrimeSpectrum.iSup_basicOpen_eq_top_iff` `Subtype.range_coe_subtype` `Set.setOf_mem_eq` `Scheme.toSpecΓ_preimage_basicOpen` `Scheme.Opens.instIsOpenImmersionι` `image_morphismRestrict_preimage` `morphismRestrict_app` `CategoryTheory.IsIso.comp_isIso'` `Scheme.Hom.image_top_eq_opensRange` `Scheme.Opens.opensRange_ι` `isIso_ΓSpec_adjunction_unit_app_basicOpen` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom`
`isIso_morphismRestrict_iff_isIso_app` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme` `Scheme.instCategory` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `morphismRestrict` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Scheme.Hom.app`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop` `IsAffineOpen.preimage` `le_rfl` `Scheme.Hom.app_eq_appLE` `Scheme.Opens.instIsOpenImmersionι` `Eq.le` `image_morphismRestrict_preimage` `morphismRestrict_app'` `Scheme.Hom.image_top_eq_opensRange` `Scheme.Opens.opensRange_ι`
`isRetrocompact_basicOpen` 📖	mathematical	—	`IsRetrocompact` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Scheme.basicOpen` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`IsRetrocompact_iff_isSpectralMap_subtypeVal` `Scheme.Hom.isSpectralMap` `instQuasiCompactOfIsAffineHom` `instIsAffineHomιBasicOpen`

AlgebraicGeometry.IsAffineHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAffine_preimage` 📖	mathematical	—	`AlgebraicGeometry.IsAffineOpen` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	—	—

AlgebraicGeometry.IsAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_pullback_inf` 📖	mathematical	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	`CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `Set` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd`	—	`isCompact_iff_compactSpace` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `Set.range_comp` `AlgebraicGeometry.Scheme.Opens.range_ι` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Hom.resLE_comp_ι` `AlgebraicGeometry.IsOpenImmersion.lift_fac` `AlgebraicGeometry.Scheme.Pullback.range_map` `AlgebraicGeometry.IsOpenImmersion.mono` `isCompact_range` `AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1` `AlgebraicGeometry.quasiCompact_of_compactSpace` `AlgebraicGeometry.quasiSeparatedSpace_of_isAffine` `AlgebraicGeometry.Scheme.compactSpace_of_isAffine` `AlgebraicGeometry.Scheme.Hom.continuous`
`preimage` 📖	mathematical	—	`AlgebraicGeometry.IsAffineOpen` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	—	`AlgebraicGeometry.IsAffineHom.isAffine_preimage`

---

← Back to Index