Module

Cartier.lean

Nyll.AlgebraicCurves.RelativeDivisors.Cartier

8 declarations indexed from sourceView source ↗

Module documentation

Cartier conditions and morphisms of ideal sheaves

Defines local invertibility of ideals and compatibility of ideal morphisms with base change.

Imports2

Imported by120

def

IsInvertible

L31 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible

Documentation

The ideal is locally generated by a non-zero-divisor on affine basic opens.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

def IsInvertible (I : X.IdealSheafData) : Prop

theorem

isInvertible_top

L35 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_top

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem isInvertible_top : (⊤ : X.IdealSheafData).IsInvertible

theorem

mul

L42 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.mul

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem IsInvertible.mul {I J : X.IdealSheafData} (hI : I.IsInvertible) (hJ : J.IsInvertible) :
    (I * J).IsInvertible

theorem

appLE_mem_comap_ideal

L72 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.appLE_mem_comap_ideal

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}
namespace IdealHom
variable {X' : Scheme.{u}} (f : X' ⟶ X) {I J : X.IdealSheafData}

Lean source · statement

theorem appLE_mem_comap_ideal (U : X.affineOpens) (U' : X'.affineOpens)
    (h : (U' : X'.Opens) ≤ f ⁻¹ᵁ U) (x : I.ideal U) :
    f.appLE U U' h x ∈ (I.comap f).ideal U'

def

IsBaseChangeAlong

L87 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.IsBaseChangeAlong

Documentation

The two ideal morphisms agree after restriction along the base change.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}
namespace IdealHom
variable {X' : Scheme.{u}} (f : X' ⟶ X) {I J : X.IdealSheafData}

Lean source · statement

def IsBaseChangeAlong (φ : IdealHom I J) (φ' : IdealHom (I.comap f) (J.comap f)) : Prop

def

IsCartier

L103 ↗

AlgebraicCurve.RelEffDivisor.IsCartier

Documentation

The relative effective divisor has a locally invertible defining ideal.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicCurve
open AlgebraicGeometry Scheme.IdealSheafData
variable {k : Type u} [Field k] {C : Scheme.{u}} {c : C ⟶ Spec (.of k)}

Lean source · statement

def RelEffDivisor.IsCartier {d : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (.of k)}
    (Z : RelEffDivisor C c d T t) : Prop

def

const

L108 ↗

AlgebraicCurve.RelEffDivisor.const

Documentation

The constant family obtained by pulling a divisor back from the field spectrum.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicCurve
open AlgebraicGeometry Scheme.IdealSheafData
variable {k : Type u} [Field k] {C : Scheme.{u}} {c : C ⟶ Spec (.of k)}

Lean source · statement

def RelEffDivisor.const {r : ℕ}
    (D : RelEffDivisor C c r (Spec (.of k)) (𝟙 _)) {T : Scheme.{u}} (t : T ⟶ Spec (.of k)) :
    RelEffDivisor C c r T t

def

FibrewiseNonvanishing

L114 ↗

AlgebraicCurve.IdealHom.FibrewiseNonvanishing

Documentation

The ideal morphism admits a compatible nonzero morphism on every fiber.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
universe u
namespace AlgebraicCurve
open AlgebraicGeometry Scheme.IdealSheafData
variable {k : Type u} [Field k] {C : Scheme.{u}} {c : C ⟶ Spec (.of k)}

Lean source · statement

def IdealHom.FibrewiseNonvanishing (c : C ⟶ Spec (.of k)) {T : Scheme.{u}}
    (t : T ⟶ Spec (.of k)) {I J : (pullback c t).IdealSheafData} (φ : IdealHom I J) : Prop

Module documentation

Cartier conditions and morphisms of ideal sheaves

Declarations