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 scheme X over a field k is geometrically P if P holds for any base change X_K for a field extension K of k.

noncomputable instance AlgebraicGeometry.instOverSpecOfOfAlgebra_geometricallyP (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (Spec (CommRingCat.of S)).Over (Spec (CommRingCat.of R))

Equations

• AlgebraicGeometry.instOverSpecOfOfAlgebra_geometricallyP R S = { hom := AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)) }

@[simp]

theorem AlgebraicGeometry.overHom_spec_self (R : Type u) [CommRing R] : Spec (CommRingCat.of R) ↘ Spec (CommRingCat.of R) = CategoryTheory.CategoryStruct.id (Spec (CommRingCat.of R))

theorem AlgebraicGeometry.overHom_Spec_def (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R) = Spec.map (CommRingCat.ofHom (algebraMap R S))

noncomputable instance AlgebraicGeometry.instOverPullbackSchemeOverInferInstanceOverClass_geometricallyP {X S T : Scheme} (f : T ⟶ S) [X.Over S] : (CategoryTheory.Limits.pullback (X ↘ S) f).Over T

If X is a scheme over S and f : T ⟶ S is a morphism, the fibre product X ×[S] T is a scheme over T. This matches the order in CategoryTheory.Over.pullback, but not the tensor product convention.

Equations

• AlgebraicGeometry.instOverPullbackSchemeOverInferInstanceOverClass_geometricallyP f = { hom := CategoryTheory.Limits.pullback.snd (X ↘ S) f }

class AlgebraicGeometry.Geometrically (P : CategoryTheory.ObjectProperty Scheme) {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : Prop

A scheme X over a field k is geometrically P if P holds for any base change X_K for a field extension K of k.

• prop_of_isPullback (K : Type u) [Field K] [Algebra k K] (Y : Scheme) (fst : Y ⟶ X) (snd : Y ⟶ Spec (CommRingCat.of K)) (h : CategoryTheory.IsPullback fst snd s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k))) : P Y

theorem AlgebraicGeometry.geometrically_iff (P : CategoryTheory.ObjectProperty Scheme) {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : Geometrically P s ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] (Y : Scheme) (fst : Y ⟶ X) (snd : Y ⟶ Spec (CommRingCat.of K)), CategoryTheory.IsPullback fst snd s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)) → P Y

@[reducible, inline]

abbrev AlgebraicGeometry.GeometricallyIsReduced {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : Prop

A scheme X over a field k is geometrically reduced if any base change X_K is reduced for a field extension K of k.

Equations

• AlgebraicGeometry.GeometricallyIsReduced s = AlgebraicGeometry.Geometrically (fun (X : AlgebraicGeometry.Scheme) => AlgebraicGeometry.IsReduced X) s

@[reducible, inline]

abbrev AlgebraicGeometry.GeometricallyConnected {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : Prop

A scheme X over a field k is geometrically connected if any base change X_K is connected for a field extension K of k.

Equations

• AlgebraicGeometry.GeometricallyConnected s = AlgebraicGeometry.Geometrically (fun (X : AlgebraicGeometry.Scheme) => ConnectedSpace ↥X) s

theorem AlgebraicGeometry.Geometrically.prop_self {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [Geometrically P s] : P X

theorem AlgebraicGeometry.Geometrically.prop_pullback {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [Geometrically P s] (K : Type u) [Field K] [Algebra k K] : P (CategoryTheory.Limits.pullback s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)))

theorem AlgebraicGeometry.Geometrically.prop_pullback' {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [Geometrically P s] (K : Type u) [Field K] [Algebra k K] : P (CategoryTheory.Limits.pullback (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)) s)

theorem AlgebraicGeometry.Geometrically.iff_of_isClosedUnderIsomorphisms {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [P.IsClosedUnderIsomorphisms] : Geometrically P s ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K], P (CategoryTheory.Limits.pullback s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)))

theorem AlgebraicGeometry.Geometrically.iff_of_iso {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [P.IsClosedUnderIsomorphisms] {Y : Scheme} (t : Y ⟶ Spec (CommRingCat.of k)) (e : X ≅ Y) (w : CategoryTheory.CategoryStruct.comp e.hom t = s := by cat_disch) : Geometrically P s ↔ Geometrically P t

theorem AlgebraicGeometry.Geometrically.of_isPullback {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [P.IsClosedUnderIsomorphisms] {k' : Type u} [Field k'] [Algebra k k'] {Y : Scheme} {fst : Y ⟶ X} {snd : Y ⟶ Spec (CommRingCat.of k')} (h : CategoryTheory.IsPullback fst snd s (Spec (CommRingCat.of k') ↘ Spec (CommRingCat.of k))) [Geometrically P s] : Geometrically P snd

If X ⟶ Spec k is geometrically P and k' is a field extension of k, then also X_k' ⟶ Spec k' is geometrically P.

theorem AlgebraicGeometry.Geometrically.iff_of_inheritedFromSource_surjective_of_isPullback {P : CategoryTheory.ObjectProperty Scheme} {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [P.InheritedFromSource @Surjective] {k' : Type u} [Field k'] [Algebra k k'] {Y : Scheme} {fst : Y ⟶ X} {snd : Y ⟶ Spec (CommRingCat.of k')} (h : CategoryTheory.IsPullback fst snd s (Spec (CommRingCat.of k') ↘ Spec (CommRingCat.of k))) : Geometrically P snd ↔ Geometrically P s

Suppose the property P is preserved by surjective morphisms (i.e., if X ⟶ Y is surjective and X satisfies P, also Y satisfies P). Then Geometrically P is invariant under scalar extensions.