Structures · Geometry
AlgebraicGeometry.IsAffineHom
A morphism of schemes X ⟶ Y is affine if
the preimage of any affine open subset of Y is affine.
- Shape
- One type argument · adds isAffine_preimage
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Every AlgebraicGeometry.IsAffineHom is also a
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Functor.obj
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.AffineSpace
- CategoryTheory.Limits.coprod
How is a type an instance?
Loading the hierarchy index…
Assumed by62
- AlgebraicGeometry.IsAffineOpen.preimage
- AlgebraicGeometry.isAffine_of_isAffineHom
- AlgebraicGeometry.exists_map_eq_top
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'
- AlgebraicGeometry.exists_map_preimage_le_map_preimage
- AlgebraicGeometry.isAffineHom_π_app
- AlgebraicGeometry.IsAffineHom.of_comp
- AlgebraicGeometry.Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D
- AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine_of_finite
- AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty'
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii'
- AlgebraicGeometry.IsAffineOpen.inf
- AlgebraicGeometry.Scheme.compactSpace_of_isLimit
- AlgebraicGeometry.Scheme.IsQuasiAffine.of_isAffineHom
- AlgebraicGeometry.exists_appTop_π_eq_of_isLimit
- AlgebraicGeometry.IsAffineHom.isAffine_preimage
- AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.g
- AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty
- AlgebraicGeometry.Scheme.exists_isQuasiAffine_of_isLimit
- AlgebraicGeometry.exists_app_map_eq_map_of_isLimit
- AlgebraicGeometry.Scheme.exists_isAffine_of_isLimit
- AlgebraicGeometry.isBasis_preimage_isAffineOpen
- AlgebraicGeometry.Scheme.nonempty_of_isLimit
- AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit
- AlgebraicGeometry.exists_preimage_eq
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq
- AlgebraicGeometry.exists_isAffineOpen_preimage_eq
- AlgebraicGeometry.IsAffine.of_isPullback
- AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ
- AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine
- AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'.congr_simp
- AlgebraicGeometry.instIsAffineHomCompScheme
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.D'
- AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc'
- AlgebraicGeometry.exists_map_preimage_eq_map_preimage
- AlgebraicGeometry.instQuasiCompactOfIsAffineHom
- AlgebraicGeometry.IsAffineHom.comp_iff
- AlgebraicGeometry.IsAffineOpen.iInf
- AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app
- AlgebraicGeometry.instIsAffineFiberOfIsAffineHom
- AlgebraicGeometry.instIsAffineHomMapOverSchemeOpensDiagram
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset
- AlgebraicGeometry.Scheme.Hom.normalization.hom_ext
- AlgebraicGeometry.IsSeparated.of_isAffineHom