Structures · Geometry
AlgebraicGeometry.IsAffine
A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.
- Defined in
- Mathlib.AlgebraicGeometry.AffineScheme
- Shape
- One type argument · adds affine
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsAffine is also a
Provided automatically by
Concrete types that are instances11
- CategoryTheory.Functor.obj
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- CategoryTheory.Limits.terminal
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.ObjectProperty.FullSubcategory.obj
- AlgebraicGeometry.Spec
- CategoryTheory.PreZeroHypercover.X
- AlgebraicGeometry.AffineSpace
- CategoryTheory.Limits.coprod
- CategoryTheory.Limits.sigmaObj
How is a type an instance?
Loading the hierarchy index…
Assumed by126
- AlgebraicGeometry.Scheme.isoSpec
- AlgebraicGeometry.isAffineOpen_top
- AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
- AlgebraicGeometry.isAffineOpen_opensRange
- AlgebraicGeometry.IsAffine.of_isIso
- AlgebraicGeometry.AffineSpace.isoOfIsAffine
- AlgebraicGeometry.isAffine_of_isAffineHom
- AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
- AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
- AlgebraicGeometry.arrowIsoSpecΓOfIsAffine
- AlgebraicGeometry.isBasis_basicOpen
- AlgebraicGeometry.HasAffineProperty.of_isPullback
- AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply
- AlgebraicGeometry.HasAffineProperty.of_openCover
- AlgebraicGeometry.HasRingHomProperty.appTop
- AlgebraicGeometry.IsAffineOpen.fromSpec_top
- AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine
- AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ
- AlgebraicGeometry.HasRingHomProperty.of_source_openCover
- AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc
- AlgebraicGeometry.AffineScheme.ofHom
- RingHom.IsStableUnderBaseChange.pullback_fst_appTop
- AlgebraicGeometry.of_targetAffineLocally_of_isPullback
- AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover
- AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine
- AlgebraicGeometry.Scheme.isAffine_of_isLimit
- AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv
- AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover
- AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine
- AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over
- AlgebraicGeometry.stalkMap_injective_of_isAffine
- AlgebraicGeometry.isIntegral_appTop_of_universallyClosed
- AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine
- AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange
- AlgebraicGeometry.HasAffineProperty.iff_of_openCover
- AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback
- AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop
- AlgebraicGeometry.Scheme.exists_isAffine_of_isLimit
- AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source
- AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus
- AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom
- AlgebraicGeometry.HasRingHomProperty.of_iSup_eq_top
- AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen
- AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus
- AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit
- AlgebraicGeometry.Scheme.isoSpec_inv_naturality
- AlgebraicGeometry.HasAffineProperty.diagonal_iff
- AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit
- AlgebraicGeometry.pointsPi_surjective_of_isAffine
- AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover
Ancestors10
- AlgebraicGeometry.IsImmersion
- AlgebraicGeometry.IsPreimmersion
- AlgebraicGeometry.IsSeparated
- AlgebraicGeometry.LocallyOfFiniteType
- AlgebraicGeometry.LocallyQuasiFinite
- AlgebraicGeometry.QuasiSeparated
- AlgebraicGeometry.Scheme.IsQuasiAffine
- AlgebraicGeometry.Scheme.IsSeparated
- AlgebraicGeometry.SurjectiveOnStalks
- CompactSpace