Module

Nonempty_pullback_sectionIdeal_pow_module_iso.lean

Nyll.JacobianVarieties.Picard.Nonempty_pullback_sectionIdeal_pow_module_iso

4 declarations indexed from sourceView source ↗

Module documentation

Compatibility of powers of the section ideal and their module sheaves with base change.

Imports13

Imported by2

theorem

comap_pow

L51 ↗

JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso.AlgebraicGeometry.RelPicard.IdealBC.comap_pow

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

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

theorem

sectionIdeal_comap

L61 ↗

JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso.AlgebraicGeometry.RelPicard.IdealBC.sectionIdeal_comap

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem 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

isInvertible_sectionIdeal

L79 ↗

JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso.AlgebraicGeometry.RelPicard.IdealBC.isInvertible_sectionIdeal

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Nonempty_pullback_sectionIdeal_pow_module_iso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem isInvertible_sectionIdeal (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T : Scheme.{u}} (t : T ⟶ Spec
      (CommRingCat.of R)) :
    (RelPicard.sectionIdeal c ε t).IsInvertible

theorem