Structures · Geometry
AlgebraicGeometry.IsIntegral
A scheme X is integral if its is nonempty,
and 𝒪ₓ(U) is an integral domain for each U ≠ ∅.
- Defined in
- Mathlib.AlgebraicGeometry.Properties
- Shape
- One type argument · adds nonempty, component_integral
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every AlgebraicGeometry.IsIntegral is also a
Concrete types that are instances6
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Spec
- AlgebraicGeometry.AffineSpace
- AlgebraicGeometry.Scheme.Hom.normalization
How is a type an instance?
Loading the hierarchy index…
Assumed by54
- AlgebraicGeometry.Scheme.ord
- AlgebraicGeometry.Scheme.ordHom
- AlgebraicGeometry.Scheme.ord_eq_zero_of_coheight_neq_one
- AlgebraicGeometry.Scheme.ord_eq_unzero_ordHom
- AlgebraicGeometry.Scheme.ord_eq_ordHom_of_coheight_eq_one
- AlgebraicGeometry.Scheme.ord.congr_simp
- AlgebraicGeometry.Scheme.ord_eq_iff
- AlgebraicGeometry.Scheme.ord_le_ord_iff
- AlgebraicGeometry.Scheme.ord_zero
- AlgebraicGeometry.isIntegral_of_isOpenImmersion
- AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField
- AlgebraicGeometry.germ_injective_of_isIntegral
- AlgebraicGeometry.Scheme.ordHom_of_isUnit
- AlgebraicGeometry.isField_of_universallyClosed
- AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
- AlgebraicGeometry.isField_of_isIntegral_of_subsingleton
- AlgebraicGeometry.Scheme.RationalMap.ofFunctionField
- AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint
- AlgebraicGeometry.map_injective_of_isIntegral
- AlgebraicGeometry.IsIntegral.component_integral
- AlgebraicGeometry.instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian
- AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen
- AlgebraicGeometry.Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral
- AlgebraicGeometry.isReduced_of_isIntegral
- AlgebraicGeometry.IsIntegral.of_isIso
- AlgebraicGeometry.instIsGermInjectiveOfIsIntegral
- AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_subsingleton
- AlgebraicGeometry.Scheme.RationalMap.eq_of_fromFunctionField_eq
- AlgebraicGeometry.self_of_isIntegral_of_geometrically
- AlgebraicGeometry.Scheme.RationalMap.equivFunctionField
- AlgebraicGeometry.instFieldCarrierFunctionField
- AlgebraicGeometry.Scheme.RationalMap.equivFunctionFieldOver
- AlgebraicGeometry.Scheme.le_ord_iff
- AlgebraicGeometry.instOrderTopCarrierCarrierCommRingCatOfIsIntegral
- AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat
- AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian
- AlgebraicGeometry.Scheme.germToFunctionField_injective
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1
- AlgebraicGeometry.finite_appTop_of_universallyClosed
- AlgebraicGeometry.Scheme.ordHom.congr_simp
- AlgebraicGeometry.Scheme.ord_mul
- AlgebraicGeometry.Scheme.ord_add
- AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral
- AlgebraicGeometry.IsIntegral.nonempty
- AlgebraicGeometry.Scheme.Hom.instIsIntegralNormalization
- AlgebraicGeometry.irreducibleSpace_of_isIntegral
- AlgebraicGeometry.exists_isUnit_germ_eq
- AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_ofFunctionField
- AlgebraicGeometry.AffineSpace.instIsIntegral