Module

AlgEquivZeroCut.lean

Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroCut

10 declarations indexed from sourceView source ↗

Module documentation

Fibrewise algebraic equivalence to zero and its pullback-stable condition on rigidified line bundles.

Imports4

Nyll.AlgebraicCurves.Geometry.Picard.Functor
Mathlib.AlgebraicGeometry.Geometrically.Integral
Nyll.AlgebraicCurves.Geometry.Picard.SubPicCondition
Mathlib.FieldTheory.IsAlgClosed.Basic

Imported by240

def

fibreAt

L34 ↗

AlgebraicGeometry.RelPicard.fibreAt

Documentation

The fibre morphism of the scalar-extended curve over a field-valued point of the test scheme.

Source context 4 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def fibreAt {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (t : T ⟶ Spec
    (CommRingCat.of R))
    {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) :
    pullback (pullback.snd c t) s ⟶ Spec (CommRingCat.of k)

def

IsAlgEquivZero

L43 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero

Documentation

A line bundle is connected to the unit by an invertible family over a geometrically integral parameter scheme locally of finite type.

Source context 4 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def IsAlgEquivZero {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k)) (L
    : A.Modules) : Prop

def

FibrewiseAlgEquivZero

L60 ↗

AlgebraicGeometry.RelPicard.FibrewiseAlgEquivZero

Documentation

The underlying line bundle is algebraically equivalent to zero on every algebraically closed field-valued fibre.

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

def FibrewiseAlgEquivZero {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (M :
    RigidifiedLineBundle c ε t) : Prop

theorem

of_iso

L66 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero.of_iso

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem IsAlgEquivZero.of_iso {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec
    (CommRingCat.of k)}
    {L L' : A.Modules} (e : L ≅ L') (hL : IsAlgEquivZero a L) : IsAlgEquivZero a L'

theorem

pullback

L72 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero.pullback

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem IsAlgEquivZero.pullback {k : Type u} [Field k] {A A' : Scheme.{u}} {a : A ⟶ Spec
    (CommRingCat.of k)}
    {a' : A' ⟶ Spec (CommRingCat.of k)} (e : A' ⟶ A) (he : e ≫ a = a') {L : A.Modules}
    (hL : IsAlgEquivZero a L) : IsAlgEquivZero a' ((Scheme.Modules.pullback e).obj L)

theorem

geometricallyIntegral_id_Spec

L104 ↗

AlgebraicGeometry.RelPicard.geometricallyIntegral_id_Spec

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem geometricallyIntegral_id_Spec (k : Type u) [Field k] :
    GeometricallyIntegral (𝟙 (Spec (CommRingCat.of k)))

theorem

fibrewiseAlgEquivZero_unit

L111 ↗

AlgebraicGeometry.RelPicard.fibrewiseAlgEquivZero_unit

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem fibrewiseAlgEquivZero_unit {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    FibrewiseAlgEquivZero (RigidifiedLineBundle.unit (c := c) (ε := ε) t)

theorem

congr

L122 ↗

AlgebraicGeometry.RelPicard.FibrewiseAlgEquivZero.congr

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem FibrewiseAlgEquivZero.congr {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {M M' : RigidifiedLineBundle c ε t} (h : Nonempty (M.L ≅ M'.L)) (hM : FibrewiseAlgEquivZero M) :
    FibrewiseAlgEquivZero M'

theorem

pullback

L128 ↗

AlgebraicGeometry.RelPicard.FibrewiseAlgEquivZero.pullback

Source context 5 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c}

Lean source · statement

theorem FibrewiseAlgEquivZero.pullback {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) {M : RigidifiedLineBundle c ε t}
    (hM : FibrewiseAlgEquivZero M) : FibrewiseAlgEquivZero (M.pullbackAlong ψ)

def