Module

RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback

3 declarations indexed from sourceView source ↗

Module documentation

Compare twisting and pullback for relative effective Cartier divisors.

Imports16

Imported by9

theorem

lbT_comap_pow

L47 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback.lbT_comap_pow

Source context 9 commands

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

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

Lean source · statement

theorem lbT_comap_pow {X Y : Scheme.{u}} (I : Y.IdealSheafData) (f : X ⟶ Y) (n : ℕ) :
    (I ^ n).comap f = (I.comap f) ^ n

theorem

lbT_sectionIdeal_comap

L55 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback.lbT_sectionIdeal_comap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem lbT_sectionIdeal_comap (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T T' : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) :
    (RelPicard.sectionIdeal c ε t).comap (RelPicard.baseChangeSnd c ψ) =
      RelPicard.sectionIdeal c ε t'

theorem

nonempty_twistModule_pullbackAlong_iso_pullback

L73 ↗

AlgebraicGeometry.RelEffCartierDiv.nonempty_twistModule_pullbackAlong_iso_pullback

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_nonempty_twistModule_pullbackAlong_iso_pullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem
_root_.AlgebraicGeometry.RelEffCartierDiv.nonempty_twistModule_pullbackAlong_iso_pullback
    (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {r : ℕ} {T T' : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) (D : RelEffCartierDiv c r t) :
    Nonempty ((D.pullbackAlong ψ.1 ψ.2).twistModule c ε ≅
      (Scheme.Modules.pullback (RelPicard.baseChangeSnd c ψ)).obj (D.twistModule c ε))

Module documentation

Declarations

lbT_comap_pow

lbT_sectionIdeal_comap

nonempty_twistModule_pullbackAlong_iso_pullback