Geometrically-P schemes over a field

In this file we define the basic interface for properties like geometrically reduced, geometrically irreducible, geometrically connected etc. In this file we treat an abstract property of schemes P and derive the general properties that are shared by all of these variants.

A morphism of schemes f : X ⟶ Y is geometrically P if for any field K and morphism Spec K ⟶ Y, the base change X ×[Y] Spec K satisfies P.

Main definitions and results

• AlgebraicGeometry.geometrically: The morphism property of geometrically-P morphisms
• AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField: f : X ⟶ Y is geometrically-P if and only if for every y : Y, the fiber f ⁻¹ {y} is geometrically-P over Spec κ(y).

Notes

This contribution was created as part of the Formalising Algebraic Geometry workshop 2025 in Heidelberg.

def AlgebraicGeometry.geometrically (P : CategoryTheory.ObjectProperty Scheme) : CategoryTheory.MorphismProperty Scheme

A morphism of schemes f : X ⟶ Y is geometrically P if for any field K and morphism Spec K ⟶ Y, the base change X ×[Y] Spec K satisfies P.

theorem AlgebraicGeometry.geometrically_eq_universally (P : CategoryTheory.ObjectProperty Scheme) : geometrically P = CategoryTheory.MorphismProperty.universally fun (X Y : Scheme) (x : X ⟶ Y) => IsIntegral Y → Subsingleton ↥Y → P X

theorem AlgebraicGeometry.geometrically_inf (P Q : CategoryTheory.ObjectProperty Scheme) : geometrically (P ⊓ Q) = geometrically P ⊓ geometrically Q

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometrically (P : CategoryTheory.ObjectProperty Scheme) : (geometrically P).IsStableUnderBaseChange

instance AlgebraicGeometry.instIsZariskiLocalAtTargetGeometricallyOfIsClosedUnderIsomorphismsScheme (P : CategoryTheory.ObjectProperty Scheme) [P.IsClosedUnderIsomorphisms] : IsZariskiLocalAtTarget (geometrically P)

theorem AlgebraicGeometry.pullback_of_geometrically {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : geometrically P f) (K : Type u) [Field K] (y : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Y) : P (CategoryTheory.Limits.pullback f y)

theorem AlgebraicGeometry.pullback_of_geometrically' {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : geometrically P f) (K : Type u) [Field K] (y : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Y) : P (CategoryTheory.Limits.pullback y f)

theorem AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} [P.IsClosedUnderIsomorphisms] : geometrically P f ↔ ∀ (K : Type u) [inst : Field K] (y : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Y), P (CategoryTheory.Limits.pullback f y)

theorem AlgebraicGeometry.fiber_of_geometrically {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : geometrically P f) (y : ↥Y) : P (Scheme.Hom.fiber f y)

theorem AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} : geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

P holds geometrically for f if and only if all fibers are geometrically P.

theorem AlgebraicGeometry.self_of_isIntegral_of_geometrically {P : CategoryTheory.ObjectProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} [IsIntegral Y] [Subsingleton ↥Y] (hf : geometrically P f) : P X

This holds in particular if Y = Spec K.

theorem AlgebraicGeometry.geometrically_iff_of_commRing {X : Scheme} {P : CategoryTheory.ObjectProperty Scheme} {R : Type u} [CommRing R] {f : X ⟶ Spec { carrier := R, commRing := inst✝ }} : geometrically P f ↔ ∀ ⦃K : Type u⦄ [inst : Field K] [inst_1 : Algebra R K] ⦃Y : Scheme⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }), CategoryTheory.IsPullback fst snd f (Spec.map (CommRingCat.ofHom (algebraMap R K))) → P Y

theorem AlgebraicGeometry.geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms {X : Scheme} {P : CategoryTheory.ObjectProperty Scheme} {R : Type u} [CommRing R] {f : X ⟶ Spec { carrier := R, commRing := inst✝ }} [P.IsClosedUnderIsomorphisms] : geometrically P f ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (CategoryTheory.Limits.pullback f (Spec.map (CommRingCat.ofHom (algebraMap R K))))