Module

RelEffCartierDivTwist2.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivTwist2

3 declarations indexed from sourceView source ↗

Module documentation

Twisting by relative effective Cartier divisors.

Imports3

Imported by30

theorem

rigSection_eq_graphOver

L31 ↗

AlgebraicGeometry.RelPicard.rigSection_eq_graphOver

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · full declaration

theorem RelPicard.rigSection_eq_graphOver (c : C ⟶ Spec (CommRingCat.of R))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    RelPicard.rigSection c t ε =
      graphOver c (t ≫ ε.1) (by rw [Category.assoc, ε.2, Category.comp_id]) := rfl

def

twistModule

L38 ↗

AlgebraicGeometry.RelEffCartierDiv.twistModule

Documentation

The rigidified divisor line module twisted by the base-point ideal to the divisor degree.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

def RelEffCartierDiv.twistModule (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {r : ℕ} {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t) : (pullback c t).Modules

theorem

twistModule_def

L44 ↗

AlgebraicGeometry.RelEffCartierDiv.twistModule_def

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem RelEffCartierDiv.twistModule_def (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {r : ℕ} {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t) :
    D.twistModule c ε = Scheme.Modules.rigidify (RelPicard.rigSection c t ε) (pullback.snd c t)
      (D.lineBundle ⊗ ((RelPicard.sectionIdeal c ε t) ^ r).module)

Module documentation

Declarations

rigSection_eq_graphOver

twistModule

twistModule_def