Varieties over a field

3 fully proved

Algebraic Geometry

ClassGeometrically reduced variety over a field#✓fully proved

Let \(k\) be a field. A scheme \(X\) with a chosen structure morphism \(X \to \operatorname{Spec} k\) is a variety over \(k\) if this morphism is separated, of finite type (quasi-compact and locally of finite type), and geometrically reduced.

class IsVariety (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))] : Prop where
  /-- The structure morphism `X ⟶ Spec k` is separated. -/
  isSeparated : IsSeparated (X ↘ Spec (CommRingCat.of k))
  /-- The structure morphism `X ⟶ Spec k` is locally of finite type. -/
  locallyOfFiniteType : LocallyOfFiniteType (X ↘ Spec (CommRingCat.of k))
  /-- The structure morphism `X ⟶ Spec k` is quasi-compact. -/
  quasiCompact : QuasiCompact (X ↘ Spec (CommRingCat.of k))
  /-- The structure morphism `X ⟶ Spec k` is geometrically reduced. -/
  geometricallyReduced : GeometricallyReduced (X ↘ Spec (CommRingCat.of k))

Used by 2

Used byCharacterization of varieties · Varieties are quasi-separated

Is Variety

TheoremCharacterization of varieties#✓fully proved

Let \(k\) be a field and let \(X\) be a scheme with a structure morphism \(X \to \operatorname{Spec} k\). Then \(X\) is a variety over \(k\) if and only if this structure morphism is separated, locally of finite type, quasi-compact and geometrically reduced.

theorem isVariety_iff :
    IsVariety k X ↔
      IsSeparated (X ↘ Spec (CommRingCat.of k)) ∧
        LocallyOfFiniteType (X ↘ Spec (CommRingCat.of k)) ∧
          QuasiCompact (X ↘ Spec (CommRingCat.of k)) ∧
            GeometricallyReduced (X ↘ Spec (CommRingCat.of k))

Uses 1

Statement usesGeometrically reduced variety over a field

TheoremVarieties are quasi-separated#✓fully proved

If \(X\) is a variety over a field \(k\), then its structure morphism \(X \to \operatorname{Spec} k\) is quasi-separated, since it is separated.

theorem quasiSeparated [IsVariety k X] :
    QuasiSeparated (X ↘ Spec (CommRingCat.of k))

Uses 1

Statement usesGeometrically reduced variety over a field

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.