Module

RelEffCartierDiv_isInvertible_I_ofPoint_of_range_subset.lean

Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isInvertible_I_ofPoint_of_range_subset

6 declarations indexed from sourceView source ↗

Module documentation

Invertibility of the ideal of a point on the smooth locus

The point ideal is invertible after restriction to the smooth open and is the unit ideal on the complement of the graph. These two descriptions give an invertible ideal globally.

Imports5

Imported by1

Nyll.JacobianVarieties.Picard.All

def

jV

L37 ↗

JacobianVarieties.Picard.Proofs.PointIdealInvertibility.SectInvAux.jV

Documentation

The open immersion on the pullbacks induced by an open of the curve.

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace SectInvAux

Lean source · statement

def jV {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) (V : C.Opens)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : pullback (V.ι ≫ c) t ⟶ pullback c t

instance

(anonymous instance)

L43 ↗

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace SectInvAux

Lean source · statement

instance {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) (V : C.Opens)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : IsOpenImmersion (jV c V t)

lemma

jV_fst

L48 ↗

JacobianVarieties.Picard.Proofs.PointIdealInvertibility.SectInvAux.jV_fst

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace SectInvAux

Lean source · statement

lemma jV_fst {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) (V : C.Opens)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    jV c V t ≫ pullback.fst c t = pullback.fst _ _ ≫ V.ι

lemma

jV_snd

L54 ↗

JacobianVarieties.Picard.Proofs.PointIdealInvertibility.SectInvAux.jV_snd

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace SectInvAux

Lean source · statement

lemma jV_snd {R : Type u} [CommRing R] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) (V : C.Opens)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    jV c V t ≫ pullback.snd c t = pullback.snd _ _ ≫ 𝟙 T

lemma

isPullback_of_fac

L60 ↗

JacobianVarieties.Picard.Proofs.PointIdealInvertibility.SectInvAux.isPullback_of_fac

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace SectInvAux

Lean source · statement

lemma isPullback_of_fac {P X Y : Scheme.{u}} (γ' : P ⟶ Y) (j : Y ⟶ X) [Mono j]
    (γ : P ⟶ X) (h : γ' ≫ j = γ) :
    IsPullback γ' (𝟙 P) j γ

theorem

isInvertible_I_ofPoint_of_range_subset

L76 ↗

AlgebraicGeometry.RelEffCartierDiv.isInvertible_I_ofPoint_of_range_subset

Source context 6 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointIdealInvertibility
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open scoped _root_.JacobianVarieties.Picard.Proofs.PointIdealInvertibility.SectInvAux
open SectInvAux in

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isInvertible_I_ofPoint_of_range_subset
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (V : C.Opens) [SmoothOfRelativeDimension 1 (V.ι ≫ c)]
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (a : T ⟶ C) (ha : a ≫ c = t)
    (hV : Set.range a.base ⊆ (V : Set C)) :
    (RelEffCartierDiv.ofPoint c a ha).I.IsInvertible

Module documentation

Invertibility of the ideal of a point on the smooth locus

Declarations

jV

(anonymous instance)

jV_fst

jV_snd

isPullback_of_fac

isInvertible_I_ofPoint_of_range_subset