Structures · Geometry
AlgebraicGeometry.IsIntegralHom
A morphism of schemes X ⟶ Y is integral if the preimage of any affine open subset of Y is
affine and the induced ring hom on sections is integral.
- Shape
- One type argument · adds isIntegral_app
Extends1
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsIntegralHom is also a
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.Limits.coprod
- AlgebraicGeometry.Scheme.Hom.normalization
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- AlgebraicGeometry.Scheme.Hom.normalizationDesc
- AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc
- AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationDesc_assoc
- AlgebraicGeometry.IsIntegralHom.isIntegral_app
- AlgebraicGeometry.IsIntegralHom.of_comp
- AlgebraicGeometry.Scheme.Hom.normalizationDesc.congr_simp
- AlgebraicGeometry.IsIntegralHom.instMorphismRestrict
- AlgebraicGeometry.IsIntegralHom.toIsAffineHom
- AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp_assoc
- AlgebraicGeometry.IsIntegralHom.comp_iff
- AlgebraicGeometry.IsIntegralHom.instDescScheme
- AlgebraicGeometry.IsIntegralHom.instSndScheme
- AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom
- AlgebraicGeometry.IsIntegralHom.instCompScheme
- AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationDesc
- AlgebraicGeometry.IsIntegralHom.instUniversallyClosed
- AlgebraicGeometry.Scheme.Hom.isIntegral_app
- AlgebraicGeometry.IsIntegralHom.instFstScheme