Module

UniversalData.lean

Nyll.AlgebraicCurves.RelativeDivisors.UniversalData

16 declarations indexed from sourceView source ↗

Module documentation

Relative effective divisors and universal families

Defines finite flat divisors, their pullbacks, and the data of a universal divisor family.

Imports7

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Properties

Imported by3

structure

RelEffDivisor

L36 ↗

AlgebraicCurve.RelEffDivisor

Documentation

An effective divisor of degree r whose projection to the base is finite and flat.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · full declaration

structure RelEffDivisor (C : Scheme.{u}) (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
    (T : Scheme.{u}) (t : T ⟶ Spec (CommRingCat.of k)) where
  /-- The ideal sheaf defining the divisor in the base changed curve. -/
  I : (pullback c t).IdealSheafData
  /-- The projection of the divisor to the base is finite. -/
  isFinite : IsFinite (I.subschemeι ≫ pullback.snd c t)
  /-- The projection of the divisor to the base is flat. -/
  flat : Flat (I.subschemeι ≫ pullback.snd c t)
  /-- Every fiber of the divisor has dimension r over the residue field. -/
  finrank_eq : ∀ s : T, (I.subschemeι ≫ pullback.snd c t).finrank s = r

lemma

ext

L47 ↗

AlgebraicCurve.RelEffDivisor.ext

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma RelEffDivisor.ext {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} {D₁ D₂ : RelEffDivisor C c r T t}
    (h : D₁.I = D₂.I) : D₁ = D₂

def

mapOnProd

L53 ↗

AlgebraicCurve.mapOnProd

Documentation

The morphism of base changed curves induced by a morphism over the field.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

def mapOnProd {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    {T Csym : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    {csym : Csym ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym) (hφ : φ ≫ csym = t) :
    pullback c t ⟶ pullback c csym

lemma

mapOnProd_fst

L60 ↗

AlgebraicCurve.mapOnProd_fst

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma mapOnProd_fst {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    {T Csym : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    {csym : Csym ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym) (hφ : φ ≫ csym = t) :
    mapOnProd c φ hφ ≫ pullback.fst c csym = pullback.fst c t

lemma

mapOnProd_snd

L66 ↗

AlgebraicCurve.mapOnProd_snd

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma mapOnProd_snd {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    {T Csym : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    {csym : Csym ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym) (hφ : φ ≫ csym = t) :
    mapOnProd c φ hφ ≫ pullback.snd c csym = pullback.snd c t ≫ φ

lemma

isPullback_mapOnProd

L72 ↗

AlgebraicCurve.isPullback_mapOnProd

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma isPullback_mapOnProd {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    {T Csym : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    {csym : Csym ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym) (hφ : φ ≫ csym = t) :
    IsPullback (mapOnProd c φ hφ) (pullback.snd c t) (pullback.snd c csym) φ

def

PullsBack

L82 ↗

AlgebraicCurve.PullsBack

Documentation

The divisor is the pullback of the given family along the specified base morphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

def PullsBack {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    (Dcan : RelEffDivisor C c r Csym csym)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) (D' : RelEffDivisor C c r T t) : Prop

def

comapSubschemeMap

L96 ↗

AlgebraicCurve.comapSubschemeMap

Documentation

The morphism from the pulled back subscheme to the original subscheme.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]
section transport
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}

Lean source · statement

def comapSubschemeMap (I : (pullback c csym).IdealSheafData) (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) : (I.comap (mapOnProd c φ hφ)).subscheme ⟶ I.subscheme

lemma

isPullback_comapSubschemeMap

L100 ↗

AlgebraicCurve.isPullback_comapSubschemeMap

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]
section transport
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}

Lean source · statement

lemma isPullback_comapSubschemeMap (I : (pullback c csym).IdealSheafData) (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) :
    IsPullback (comapSubschemeMap I φ hφ) (I.comap (mapOnProd c φ hφ)).subschemeι
      I.subschemeι (mapOnProd c φ hφ)

lemma

isPullback_comap_snd

L109 ↗

AlgebraicCurve.isPullback_comap_snd

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]
section transport
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}

Lean source · statement

lemma isPullback_comap_snd (I : (pullback c csym).IdealSheafData) (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) :
    IsPullback (comapSubschemeMap I φ hφ)
      ((I.comap (mapOnProd c φ hφ)).subschemeι ≫ pullback.snd c t)
      (I.subschemeι ≫ pullback.snd c csym) φ

def

pullbackAlong

L119 ↗

AlgebraicCurve.RelEffDivisor.pullbackAlong

Documentation

The finite flat divisor obtained by pulling back along a morphism over the field.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · full declaration

def RelEffDivisor.pullbackAlong {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    (Dcan : RelEffDivisor C c r Csym csym)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) : RelEffDivisor C c r T t where
  I := Dcan.I.comap (mapOnProd c φ hφ)
  isFinite :=
    have := Dcan.isFinite
    MorphismProperty.of_isPullback (isPullback_comap_snd Dcan.I φ hφ) ‹_›
  flat :=
    have := Dcan.flat
    MorphismProperty.of_isPullback (isPullback_comap_snd Dcan.I φ hφ) ‹_›
  finrank_eq s := by
    have := Dcan.isFinite
    have := Dcan.flat
    rw [Scheme.Hom.finrank_of_isPullback _ _ _ _ (isPullback_comap_snd Dcan.I φ hφ) s]
    exact Dcan.finrank_eq (φ s)

theorem

pullsBack_pullbackAlong

L138 ↗

AlgebraicCurve.pullsBack_pullbackAlong

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

theorem pullsBack_pullbackAlong {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {r : ℕ} {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    (Dcan : RelEffDivisor C c r Csym csym)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym)
    (hφ : φ ≫ csym = t) :
    PullsBack Dcan φ hφ (Dcan.pullbackAlong φ hφ)

lemma

eq_pullbackAlong

L145 ↗

AlgebraicCurve.PullsBack.eq_pullbackAlong

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma PullsBack.eq_pullbackAlong {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {r : ℕ} {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    {Dcan : RelEffDivisor C c r Csym csym}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} {φ : T ⟶ Csym}
    {hφ : φ ≫ csym = t} {D' : RelEffDivisor C c r T t} (h : PullsBack Dcan φ hφ D') :
    D' = Dcan.pullbackAlong φ hφ

lemma

isPullback

L153 ↗

AlgebraicCurve.PullsBack.isPullback

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · statement

lemma PullsBack.isPullback {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    {Dcan : RelEffDivisor C c r Csym csym}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} {φ : T ⟶ Csym}
    {hφ : φ ≫ csym = t} {D' : RelEffDivisor C c r T t} (h : PullsBack Dcan φ hφ D') :
    ∃ ψ : D'.I.subscheme ⟶ Dcan.I.subscheme,
      IsPullback ψ (D'.I.subschemeι ≫ pullback.snd c t)
        (Dcan.I.subschemeι ≫ pullback.snd c csym) φ

lemma

pullbackAlong_comp

L164 ↗

AlgebraicCurve.RelEffDivisor.pullbackAlong_comp

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · full declaration

lemma RelEffDivisor.pullbackAlong_comp {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {Csym : Scheme.{u}} {csym : Csym ⟶ Spec (CommRingCat.of k)}
    (Dcan : RelEffDivisor C c r Csym csym)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ Csym) (hφ : φ ≫ csym = t)
    {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of k)} (φ' : T' ⟶ T)
    (hφ' : φ' ≫ t = t') :
    (Dcan.pullbackAlong φ hφ).pullbackAlong φ' hφ' =
      Dcan.pullbackAlong (φ' ≫ φ) (by rw [Category.assoc, hφ, hφ']) := by
  refine RelEffDivisor.ext ?_
  change (Dcan.I.comap _).comap _ = Dcan.I.comap _
  rw [← Scheme.IdealSheafData.comap_comp]
  congr 1
  ext <;> simp

structure

UnivDivisorPack

L180 ↗

AlgebraicCurve.UnivDivisorPack

Documentation

A divisor family with existence on integral bases and uniqueness on reduced bases.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace AlgebraicCurve
variable {k : Type u} [Field k]

Lean source · full declaration

structure UnivDivisorPack (C : Scheme.{u}) (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)
    (Csym : Scheme.{u}) (csym : Csym ⟶ Spec (CommRingCat.of k)) where
  /-- The distinguished divisor family on the parameter scheme. -/
  Dcan : RelEffDivisor C c r Csym csym
  /-- Each divisor on an integral base is pulled back from the distinguished family. -/
  exists_pullsBack : ∀ (T : Scheme.{u}) (t : T ⟶ Spec (CommRingCat.of k)) [IsIntegral T]
    [LocallyOfFiniteType t] [QuasiCompact t] (D' : RelEffDivisor C c r T t),
    ∃ (φ : T ⟶ Csym) (hφ : φ ≫ csym = t), PullsBack Dcan φ hφ D'
  /-- Two morphisms defining the same pulled back family on a reduced base are equal. -/
  eq_of_pullsBack : ∀ (T : Scheme.{u}) (t : T ⟶ Spec (CommRingCat.of k)) [IsReduced T]
    [LocallyOfFiniteType t] [QuasiCompact t] (D' : RelEffDivisor C c r T t)
    (φ₁ φ₂ : T ⟶ Csym) (hφ₁ : φ₁ ≫ csym = t) (hφ₂ : φ₂ ≫ csym = t),
    PullsBack Dcan φ₁ hφ₁ D' → PullsBack Dcan φ₂ hφ₂ D' → φ₁ = φ₂

Module documentation

Relative effective divisors and universal families

Declarations