Module

RelEffCartierDivSum.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSum

29 declarations indexed from sourceView source ↗

Module documentation

Divisors defined by products of section ideals

Defines sums of section divisors, fiber powers, and their tautological ideal.

Imports3

Mathlib.AlgebraicGeometry.Limits
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivOfPoint
Nyll.AlgebraicCurves.Hilbert.SymmetricPowerData

Imported by33

abbrev

fibrePowOver

L32 ↗

AlgebraicGeometry.fibrePowOver

Documentation

The fiber product of r copies of the curve over the base.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)

Lean source · statement

abbrev fibrePowOver : Scheme.{u}

abbrev

proj

L38 ↗

AlgebraicGeometry.fibrePowOver.proj

Documentation

The projection from the fiber power to its i-th factor.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
namespace fibrePowOver

Lean source · statement

abbrev proj (i : Fin r) : fibrePowOver f r ⟶ 𝒞

abbrev

toBase

L42 ↗

AlgebraicGeometry.fibrePowOver.toBase

Documentation

The structure morphism from the fiber power to the base.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
namespace fibrePowOver

Lean source · statement

abbrev toBase : fibrePowOver f r ⟶ S

theorem

proj_comp

L45 ↗

AlgebraicGeometry.fibrePowOver.proj_comp

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
namespace fibrePowOver

Lean source · statement

theorem proj_comp (i : Fin r) : proj f r i ≫ f = toBase f r

def

prodKerGraph

L53 ↗

AlgebraicGeometry.prodKerGraph

Documentation

The product of the ideal sheaves of the graphs of the given sections.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

def prodKerGraph (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    (pullback f g).IdealSheafData

theorem

prodKerGraph_eq_prod

L57 ↗

AlgebraicGeometry.prodKerGraph_eq_prod

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

theorem prodKerGraph_eq_prod (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    prodKerGraph f a ha = ∏ i, (graphOver f (a i) (ha i)).ker

theorem

prodKerGraph_zero

L61 ↗

AlgebraicGeometry.prodKerGraph_zero

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

theorem prodKerGraph_zero (a : Fin 0 → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    prodKerGraph f a ha = ⊤

theorem

prodKerGraph_one

L65 ↗

AlgebraicGeometry.prodKerGraph_one

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

theorem prodKerGraph_one (a : Fin 1 → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    prodKerGraph f a ha = (graphOver f (a 0) (ha 0)).ker

theorem

prodKerGraph_succ

L69 ↗

AlgebraicGeometry.prodKerGraph_succ

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · full declaration

theorem prodKerGraph_succ (a : Fin (r + 1) → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    prodKerGraph f a ha =
      (graphOver f (a 0) (ha 0)).ker * prodKerGraph f (fun i => a i.succ) (fun i => ha i.succ) := by
  simp [prodKerGraph, Fin.prod_univ_succ]

theorem

prodKerGraph_comp_equiv

L74 ↗

AlgebraicGeometry.prodKerGraph_comp_equiv

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · full declaration

theorem prodKerGraph_comp_equiv (σ : Equiv.Perm (Fin r)) (a : Fin r → (T ⟶ 𝒞))
    (ha : ∀ i, a i ≫ f = g) :
    prodKerGraph f (fun i => a (σ i)) (fun i => ha (σ i)) = prodKerGraph f a ha :=
  Equiv.prod_comp σ (fun i => (graphOver f (a i) (ha i)).ker)

theorem

ideal_prodKerGraph

L79 ↗

AlgebraicGeometry.ideal_prodKerGraph

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

theorem ideal_prodKerGraph (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g)
    (U : (pullback f g).affineOpens) :
    (prodKerGraph f a ha).ideal U = ∏ i, (graphOver f (a i) (ha i)).ker.ideal U

def

SameDivisor

L89 ↗

AlgebraicGeometry.SameDivisor

Documentation

The two families of sections define the same product of graph ideals.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

def SameDivisor (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) (b : Fin r → (T ⟶ 𝒞))
    (hb : ∀ i, b i ≫ f = g) : Prop

theorem

iff

L97 ↗

AlgebraicGeometry.SameDivisor.iff

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · statement

theorem iff {a : Fin r → (T ⟶ 𝒞)} {ha : ∀ i, a i ≫ f = g} {b : Fin r → (T ⟶ 𝒞)}
    {hb : ∀ i, b i ≫ f = g} :
    SameDivisor f a ha b hb ↔ prodKerGraph f a ha = prodKerGraph f b hb

theorem

refl

L102 ↗

AlgebraicGeometry.SameDivisor.refl

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · statement

theorem refl (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) : SameDivisor f a ha a ha

theorem

rfl

L105 ↗

AlgebraicGeometry.SameDivisor.rfl

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · statement

theorem rfl {a : Fin r → (T ⟶ 𝒞)} {ha : ∀ i, a i ≫ f = g} : SameDivisor f a ha a ha

theorem

symm

L108 ↗

AlgebraicGeometry.SameDivisor.symm

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · statement

theorem symm {a : Fin r → (T ⟶ 𝒞)} {ha : ∀ i, a i ≫ f = g} {b : Fin r → (T ⟶ 𝒞)}
    {hb : ∀ i, b i ≫ f = g} (h : SameDivisor f a ha b hb) : SameDivisor f b hb a ha

theorem

trans

L112 ↗

AlgebraicGeometry.SameDivisor.trans

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · statement

theorem trans {a : Fin r → (T ⟶ 𝒞)} {ha : ∀ i, a i ≫ f = g} {b : Fin r → (T ⟶ 𝒞)}
    {hb : ∀ i, b i ≫ f = g} {c : Fin r → (T ⟶ 𝒞)} {hc : ∀ i, c i ≫ f = g}
    (h₁ : SameDivisor f a ha b hb) (h₂ : SameDivisor f b hb c hc) : SameDivisor f a ha c hc

theorem

comp_equiv

L117 ↗

AlgebraicGeometry.SameDivisor.comp_equiv

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace SameDivisor
variable {f}

Lean source · full declaration

theorem comp_equiv (σ : Equiv.Perm (Fin r)) (a : Fin r → (T ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g) :
    SameDivisor f (fun i => a (σ i)) (fun i => ha (σ i)) a ha :=
  prodKerGraph_comp_equiv f σ a ha

theorem

finrank_eq_zero_of_isEmpty

L125 ↗

AlgebraicGeometry.Scheme.Hom.finrank_eq_zero_of_isEmpty

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty

Lean source · statement

theorem Scheme.Hom.finrank_eq_zero_of_isEmpty {X Y : Scheme.{u}} (π : X ⟶ Y) [IsEmpty X]
    (y : Y) : π.finrank y = 0

def

empty

L143 ↗

AlgebraicGeometry.RelEffCartierDiv.empty

Documentation

The relative effective divisor of degree zero defined by the unit ideal.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty

Lean source · full declaration

def RelEffCartierDiv.empty (g : T ⟶ S) : RelEffCartierDiv f 0 g where
  I := ⊤
  isFinite := inferInstance
  flat := inferInstance
  locallyOfFinitePresentation := inferInstance
  finrank_eq t := Scheme.Hom.finrank_eq_zero_of_isEmpty _ t

theorem

empty_I

L150 ↗

AlgebraicGeometry.RelEffCartierDiv.empty_I

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty

Lean source · statement

theorem RelEffCartierDiv.empty_I (g : T ⟶ S) : (RelEffCartierDiv.empty f g).I = ⊤

theorem

I_eq_top_of_degree_zero

L155 ↗

AlgebraicGeometry.RelEffCartierDiv.I_eq_top_of_degree_zero

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty
variable {f}

Lean source · statement

theorem RelEffCartierDiv.I_eq_top_of_degree_zero (D : RelEffCartierDiv f 0 g) : D.I = ⊤

instance

subsingleton_of_degree_zero

L168 ↗

AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty
variable {f}

Lean source · statement

instance RelEffCartierDiv.subsingleton_of_degree_zero : Subsingleton (RelEffCartierDiv f 0 g)

theorem

eq_empty

L171 ↗

AlgebraicGeometry.RelEffCartierDiv.eq_empty

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section Empty
variable {f}

Lean source · statement

theorem RelEffCartierDiv.eq_empty (D : RelEffCartierDiv f 0 g) : D = RelEffCartierDiv.empty f g

abbrev

tautIdeal

L181 ↗

AlgebraicGeometry.fibrePowOver.tautIdeal

Documentation

The product of the graph ideals of the tautological projections on the fiber power.

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
namespace fibrePowOver
variable (r)

Lean source · statement

abbrev tautIdeal : (pullback f (toBase f r)).IdealSheafData

theorem

fibrePowOver_eq_finFibrePow

L190 ↗

AlgebraicGeometry.fibrePowOver_eq_finFibrePow

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section FieldComparison
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)

Lean source · statement

theorem fibrePowOver_eq_finFibrePow : fibrePowOver c r = finFibrePow c r

theorem

proj_eq_finFibrePow_proj

L192 ↗

AlgebraicGeometry.fibrePowOver.proj_eq_finFibrePow_proj

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section FieldComparison
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)

Lean source · statement

theorem fibrePowOver.proj_eq_finFibrePow_proj (i : Fin r) :
    fibrePowOver.proj c r i = finFibrePow.proj c r i

theorem

toBase_eq_finFibrePow_toBase

L195 ↗

AlgebraicGeometry.fibrePowOver.toBase_eq_finFibrePow_toBase

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section FieldComparison
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)

Lean source · statement

theorem fibrePowOver.toBase_eq_finFibrePow_toBase :
    fibrePowOver.toBase c r = finFibrePow.toBase c r

theorem

tautIdeal_eq_prod_ker_lift

L198 ↗

AlgebraicGeometry.fibrePowOver.tautIdeal_eq_prod_ker_lift

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {r} {T : Scheme.{u}} {g : T ⟶ S}
section FieldComparison
variable {k : Type u} [Field k] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k)) (r : ℕ)

Lean source · full declaration

theorem fibrePowOver.tautIdeal_eq_prod_ker_lift :
    fibrePowOver.tautIdeal c r = ∏ i : Fin r,
      (pullback.lift (WidePullback.π (fun _ : Fin r => c) i) (𝟙 (finFibrePow c r))
        (by rw [Category.id_comp]; exact WidePullback.π_arrow _ i)).ker := rfl

Module documentation

Divisors defined by products of section ideals

Declarations