Module

RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn

1 declaration indexed from sourceView source ↗

Module documentation

Rel Eff Cartier Div is Invertible twist Module and nonempty pullback iso of supported In

Imports11

Imported by2

theorem

isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn

L88 ↗

AlgebraicGeometry.RelEffCartierDiv.isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelEffCartierDiv
universe u
open _root_.AlgebraicCurves.RelativeDivisors.Proofs in
open RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn in
open _root_.CategoryTheory in
open _root_.CategoryTheory.Limits in
open _root_.CategoryTheory.MonoidalCategory in
open _root_.AlgebraicGeometry in
open _root_.NeronModelInfra in

Lean source · statement

theorem isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)] (hεU : Set.range ε.1 ⊆ (U : Set C))
    {r : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t) (hD :
      D.SupportedIn U) :
    Scheme.Modules.IsInvertible (D.twistModule c ε) ∧
      Nonempty ((Scheme.Modules.pullback (RelPicard.rigSection c t ε)).obj (D.twistModule c ε) ≅
        𝟙_ T.Modules)

Module documentation

Rel Eff Cartier Div is Invertible twist Module and nonempty pullback iso of supported In

Declarations

isInvertible_twistModule_and_nonempty_pullback_iso_of_supportedIn