Structures · Geometry
AlgebraicGeometry.GeometricallyIrreducible
We say that morphism f : X ⟶ Y is geometrically irreducible if for all Spec K ⟶ Y with K
a field, X ×[Y] Spec K is irreducible.
- Shape
- One type argument · adds geometrically_irreducibleSpace
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every AlgebraicGeometry.GeometricallyIrreducible is also a
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.AffineSpace
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv
- AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace
- AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage
- AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen
- AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe
- AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace
- AlgebraicGeometry.instGeometricallyIrreducibleFiberToSpecResidueField
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1
- AlgebraicGeometry.instSurjectiveOfGeometricallyIrreducible
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible
- AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe
- AlgebraicGeometry.GeometricallyIrreducible.comp
- AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict
- AlgebraicGeometry.instGeometricallyIrreducibleSndScheme
- AlgebraicGeometry.instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective
- AlgebraicGeometry.instGeometricallyIrreducibleFstScheme
- AlgebraicGeometry.GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible