Module

RelEffCartierDivOfPoint.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivOfPoint

11 declarations indexed from sourceView source ↗

Module documentation

Relative divisors defined by sections

Constructs the divisor associated to the graph of a section over the base.

Imports2

Mathlib.AlgebraicGeometry.Morphisms.Separated
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by62

def

graphOver

L31 ↗

AlgebraicGeometry.graphOver

Documentation

The graph of a morphism over the base, regarded as a section of the pullback.

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

def graphOver (a : T ⟶ 𝒞) (ha : a ≫ f = g) : T ⟶ pullback f g

lemma

graphOver_eq_lift

L34 ↗

AlgebraicGeometry.graphOver_eq_lift

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma graphOver_eq_lift (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    graphOver f a ha = pullback.lift a (𝟙 T) (ha.trans (Category.id_comp g).symm)

lemma

graphOver_fst

L37 ↗

AlgebraicGeometry.graphOver_fst

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma graphOver_fst (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    graphOver f a ha ≫ pullback.fst f g = a

lemma

graphOver_snd

L41 ↗

AlgebraicGeometry.graphOver_snd

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma graphOver_snd (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    graphOver f a ha ≫ pullback.snd f g = 𝟙 T

instance

isClosedImmersion_graphOver

L45 ↗

AlgebraicGeometry.isClosedImmersion_graphOver

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

instance isClosedImmersion_graphOver [IsSeparated f] (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    IsClosedImmersion (graphOver f a ha)

instance

isIso_ker_graphOver_subschemeIota_snd

L51 ↗

AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

instance isIso_ker_graphOver_subschemeIota_snd [IsSeparated f] (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    IsIso ((graphOver f a ha).ker.subschemeι ≫ pullback.snd f g)

def

ofPoint

L61 ↗

AlgebraicGeometry.RelEffCartierDiv.ofPoint

Documentation

The relative effective Cartier divisor of degree one defined by the graph of a point.

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · full declaration

def RelEffCartierDiv.ofPoint [IsSeparated f] (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    RelEffCartierDiv f 1 g where
  I := (graphOver f a ha).ker
  isFinite := inferInstance
  flat := inferInstance
  locallyOfFinitePresentation := inferInstance
  finrank_eq t := by
    rw [Scheme.Hom.finrank_eq_one_of_isIso ((graphOver f a ha).ker.subschemeι ≫ pullback.snd f g)]
    rfl

lemma

ofPoint_I

L71 ↗

AlgebraicGeometry.RelEffCartierDiv.ofPoint_I

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) {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma RelEffCartierDiv.ofPoint_I [IsSeparated f] (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    (RelEffCartierDiv.ofPoint f a ha).I = (graphOver f a ha).ker

instance

isIso_subschemeIota_snd_of_degree_one

L75 ↗

AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_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) {T : Scheme.{u}} {g : T ⟶ S}
variable {f} in

Lean source · statement

instance RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one (D : RelEffCartierDiv f 1 g) :
    IsIso (D.I.subschemeι ≫ pullback.snd f g)

def

toPoint

L83 ↗

AlgebraicGeometry.RelEffCartierDiv.toPoint

Documentation

The point determined by a relative effective Cartier divisor of degree one.

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) {T : Scheme.{u}} {g : T ⟶ S}
variable {f} in
variable {f} in

Lean source · statement

def RelEffCartierDiv.toPoint (D : RelEffCartierDiv f 1 g) : T ⟶ 𝒞

lemma

toPoint_comp

L88 ↗

AlgebraicGeometry.RelEffCartierDiv.toPoint_comp

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) {T : Scheme.{u}} {g : T ⟶ S}
variable {f} in
variable {f} in
variable {f} in

Lean source · statement

lemma RelEffCartierDiv.toPoint_comp (D : RelEffCartierDiv f 1 g) : D.toPoint ≫ f = g

Module documentation

Relative divisors defined by sections

Declarations