Module

RelEffCartierDiv.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

23 declarations indexed from sourceView source ↗

Module documentation

Relative effective divisors and base change

Describes relative effective divisors with finite, flat, locally finitely presented projections.

Imports6

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Nyll.AlgebraicCurves.RelativeDivisors.UniversalData

Imported by123

structure

RelEffCartierDiv

L34 ↗

AlgebraicGeometry.RelEffCartierDiv

Documentation

A relative effective divisor of constant degree, with finite, flat, and locally finitely presented projection.

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · full declaration

structure RelEffCartierDiv {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
    {T : Scheme.{u}} (g : T ⟶ S) where
  /-- The ideal sheaf defining the divisor in the base changed curve. -/
  I : (pullback f g).IdealSheafData
  /-- The projection of the divisor to the base is finite. -/
  isFinite : IsFinite (I.subschemeι ≫ pullback.snd f g)
  /-- The projection of the divisor to the base is flat. -/
  flat : Flat (I.subschemeι ≫ pullback.snd f g)
  /-- The projection of the divisor is locally of finite presentation. -/
  locallyOfFinitePresentation : LocallyOfFinitePresentation (I.subschemeι ≫ pullback.snd f g)
  /-- Every fibre of the divisor has the prescribed rank. -/
  finrank_eq : ∀ t : T, (I.subschemeι ≫ pullback.snd f g).finrank t = r

lemma

ext

L47 ↗

AlgebraicGeometry.RelEffCartierDiv.ext

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma RelEffCartierDiv.ext {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T : Scheme.{u}} {g : T ⟶ S} {D₁ D₂ : RelEffCartierDiv f r g}
    (h : D₁.I = D₂.I) : D₁ = D₂

def

mapOnProdOver

L53 ↗

AlgebraicGeometry.mapOnProdOver

Documentation

The map between base changed curves induced by a morphism over the original base.

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

def mapOnProdOver {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    pullback f g ⟶ pullback f g'

lemma

mapOnProdOver_fst

L58 ↗

AlgebraicGeometry.mapOnProdOver_fst

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma mapOnProdOver_fst {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    mapOnProdOver f φ hφ ≫ pullback.fst f g' = pullback.fst f g

lemma

mapOnProdOver_snd

L63 ↗

AlgebraicGeometry.mapOnProdOver_snd

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma mapOnProdOver_snd {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    mapOnProdOver f φ hφ ≫ pullback.snd f g' = pullback.snd f g ≫ φ

lemma

mapOnProdOver_id

L68 ↗

AlgebraicGeometry.mapOnProdOver_id

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma mapOnProdOver_id {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) {T : Scheme.{u}} {g : T ⟶ S} :
    mapOnProdOver f (𝟙 T) (Category.id_comp g) = 𝟙 (pullback f g)

lemma

isPullback_mapOnProdOver

L72 ↗

AlgebraicGeometry.isPullback_mapOnProdOver

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma isPullback_mapOnProdOver {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    IsPullback (mapOnProdOver f φ hφ) (pullback.snd f g) (pullback.snd f g') φ

def

PullsBackOver

L82 ↗

AlgebraicGeometry.PullsBackOver

Documentation

The condition that one relative divisor is the pullback of another along a morphism over the base.

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

def PullsBackOver {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T' : Scheme.{u}} {g' : T' ⟶ S} (D : RelEffCartierDiv f r g')
    {T : Scheme.{u}} {g : T ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g)
    (D' : RelEffCartierDiv f r g) : Prop

def

comapSubschemeMapOver

L94 ↗

AlgebraicGeometry.comapSubschemeMapOver

Documentation

The natural map from the subscheme defined by the pulled back ideal to the original subscheme.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
section transport
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S}

Lean source · statement

def comapSubschemeMapOver (I : (pullback f g').IdealSheafData) (φ : T ⟶ T')
    (hφ : φ ≫ g' = g) : (I.comap (mapOnProdOver f φ hφ)).subscheme ⟶ I.subscheme

lemma

isPullback_comapSubschemeMapOver

L98 ↗

AlgebraicGeometry.isPullback_comapSubschemeMapOver

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
section transport
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S}

Lean source · statement

lemma isPullback_comapSubschemeMapOver (I : (pullback f g').IdealSheafData) (φ : T ⟶ T')
    (hφ : φ ≫ g' = g) :
    IsPullback (comapSubschemeMapOver I φ hφ) (I.comap (mapOnProdOver f φ hφ)).subschemeι
      I.subschemeι (mapOnProdOver f φ hφ)

lemma

isPullback_comap_snd_over

L107 ↗

AlgebraicGeometry.isPullback_comap_snd_over

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
section transport
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S}

Lean source · statement

lemma isPullback_comap_snd_over (I : (pullback f g').IdealSheafData) (φ : T ⟶ T')
    (hφ : φ ≫ g' = g) :
    IsPullback (comapSubschemeMapOver I φ hφ)
      ((I.comap (mapOnProdOver f φ hφ)).subschemeι ≫ pullback.snd f g)
      (I.subschemeι ≫ pullback.snd f g') φ

def

pullbackAlong

L117 ↗

AlgebraicGeometry.RelEffCartierDiv.pullbackAlong

Documentation

Pullback of a relative effective divisor along a morphism over the base.

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · full declaration

def RelEffCartierDiv.pullbackAlong {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T' : Scheme.{u}} {g' : T' ⟶ S} (D : RelEffCartierDiv f r g')
    {T : Scheme.{u}} {g : T ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) : RelEffCartierDiv f r g where
  I := D.I.comap (mapOnProdOver f φ hφ)
  isFinite :=
    have := D.isFinite
    MorphismProperty.of_isPullback (isPullback_comap_snd_over D.I φ hφ) ‹_›
  flat :=
    have := D.flat
    MorphismProperty.of_isPullback (isPullback_comap_snd_over D.I φ hφ) ‹_›
  locallyOfFinitePresentation :=
    have := D.locallyOfFinitePresentation
    MorphismProperty.of_isPullback (isPullback_comap_snd_over D.I φ hφ) ‹_›
  finrank_eq t := by
    have := D.isFinite
    have := D.flat
    have := D.locallyOfFinitePresentation
    rw [Scheme.Hom.finrank_of_isPullback _ _ _ _ (isPullback_comap_snd_over D.I φ hφ) t]
    exact D.finrank_eq (φ t)

theorem

pullsBackOver_pullbackAlong

L137 ↗

AlgebraicGeometry.pullsBackOver_pullbackAlong

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem pullsBackOver_pullbackAlong {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T' : Scheme.{u}} {g' : T' ⟶ S} (D : RelEffCartierDiv f r g')
    {T : Scheme.{u}} {g : T ⟶ S} (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    PullsBackOver D φ hφ (D.pullbackAlong φ hφ)

lemma

eq_pullbackAlong

L142 ↗

AlgebraicGeometry.PullsBackOver.eq_pullbackAlong

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma PullsBackOver.eq_pullbackAlong {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T' : Scheme.{u}} {g' : T' ⟶ S} {D : RelEffCartierDiv f r g'}
    {T : Scheme.{u}} {g : T ⟶ S} {φ : T ⟶ T'} {hφ : φ ≫ g' = g}
    {D' : RelEffCartierDiv f r g} (h : PullsBackOver D φ hφ D') :
    D' = D.pullbackAlong φ hφ

lemma

isPullback

L149 ↗

AlgebraicGeometry.PullsBackOver.isPullback

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma PullsBackOver.isPullback {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T' : Scheme.{u}} {g' : T' ⟶ S} {D : RelEffCartierDiv f r g'}
    {T : Scheme.{u}} {g : T ⟶ S} {φ : T ⟶ T'} {hφ : φ ≫ g' = g}
    {D' : RelEffCartierDiv f r g} (h : PullsBackOver D φ hφ D') :
    ∃ ψ : D'.I.subscheme ⟶ D.I.subscheme,
      IsPullback ψ (D'.I.subschemeι ≫ pullback.snd f g) (D.I.subschemeι ≫ pullback.snd f g') φ

lemma

pullbackAlong_comp

L158 ↗

AlgebraicGeometry.RelEffCartierDiv.pullbackAlong_comp

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · full declaration

lemma RelEffCartierDiv.pullbackAlong_comp {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T'' : Scheme.{u}} {g'' : T'' ⟶ S} (D : RelEffCartierDiv f r g'')
    {T' : Scheme.{u}} {g' : T' ⟶ S} (φ : T' ⟶ T'') (hφ : φ ≫ g'' = g')
    {T : Scheme.{u}} {g : T ⟶ S} (φ' : T ⟶ T') (hφ' : φ' ≫ g' = g) :
    (D.pullbackAlong φ hφ).pullbackAlong φ' hφ' =
      D.pullbackAlong (φ' ≫ φ) (by rw [Category.assoc, hφ, hφ']) := by
  refine RelEffCartierDiv.ext ?_
  change (D.I.comap _).comap _ = D.I.comap _
  rw [← Scheme.IdealSheafData.comap_comp]
  congr 1
  ext <;> simp

lemma

pullbackAlong_id

L170 ↗

AlgebraicGeometry.RelEffCartierDiv.pullbackAlong_id

Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry

Lean source · statement

lemma RelEffCartierDiv.pullbackAlong_id {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
    {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) :
    D.pullbackAlong (𝟙 T) (Category.id_comp g) = D

def

toRelEffDivisor

L183 ↗

AlgebraicGeometry.RelEffCartierDiv.toRelEffDivisor

Documentation

The corresponding relative effective divisor in the curve construction over a field.

Source context 5 commands

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

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

Lean source · statement

def RelEffCartierDiv.toRelEffDivisor {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {r : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (D : RelEffCartierDiv c r t) :
    AlgebraicCurve.RelEffDivisor C c r T t

lemma

toRelEffDivisor_I

L188 ↗

AlgebraicGeometry.RelEffCartierDiv.toRelEffDivisor_I

Source context 5 commands

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

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

Lean source · statement

lemma RelEffCartierDiv.toRelEffDivisor_I {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ} {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of k)} (D : RelEffCartierDiv c r t) :
    D.toRelEffDivisor.I = D.I

lemma

toRelEffDivisor_injective

L193 ↗

AlgebraicGeometry.RelEffCartierDiv.toRelEffDivisor_injective

Source context 5 commands

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

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

Lean source · statement

lemma RelEffCartierDiv.toRelEffDivisor_injective {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ} {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of k)} :
    Function.Injective (RelEffCartierDiv.toRelEffDivisor (c := c) (r := r) (t := t))

def

ofRelEffDivisor

L201 ↗

AlgebraicGeometry.RelEffCartierDiv.ofRelEffDivisor

Documentation

A relative effective divisor from the field construction with a locally finitely presented projection.

Source context 5 commands

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

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

Lean source · statement

def RelEffCartierDiv.ofRelEffDivisor {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
    {r : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    (D : AlgebraicCurve.RelEffDivisor C c r T t)
    (h : LocallyOfFinitePresentation (D.I.subschemeι ≫ pullback.snd c t)) :
    RelEffCartierDiv c r t

lemma

toRelEffDivisor_ofRelEffDivisor

L208 ↗

AlgebraicGeometry.RelEffCartierDiv.toRelEffDivisor_ofRelEffDivisor

Source context 5 commands

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

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

Lean source · statement

lemma RelEffCartierDiv.toRelEffDivisor_ofRelEffDivisor {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ} {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of k)} (D : AlgebraicCurve.RelEffDivisor C c r T t)
    (h : LocallyOfFinitePresentation (D.I.subschemeι ≫ pullback.snd c t)) :
    (RelEffCartierDiv.ofRelEffDivisor D h).toRelEffDivisor = D

lemma

toRelEffDivisor_pullbackAlong

L214 ↗

AlgebraicGeometry.RelEffCartierDiv.toRelEffDivisor_pullbackAlong

Source context 5 commands

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

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

Lean source · statement

lemma RelEffCartierDiv.toRelEffDivisor_pullbackAlong {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of k)} {r : ℕ}
    {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of k)} (D : RelEffCartierDiv c r t')
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (φ : T ⟶ T') (hφ : φ ≫ t' = t) :
    (D.pullbackAlong φ hφ).toRelEffDivisor = D.toRelEffDivisor.pullbackAlong φ hφ

Module documentation

Relative effective divisors and base change

Declarations