Module

Nonempty_pullback_sectionTwist_iso.lean

Nyll.AlgebraicCurves.Geometry.Picard.Nonempty_pullback_sectionTwist_iso

4 declarations indexed from sourceView source ↗

Module documentation

Compatibility of section ideals, their powers and associated section twists with scalar- extension pullback.

Imports9

Imported by18

theorem

stwE5_comap_pow

L73 ↗

AlgebraicGeometry.stwE5_comap_pow

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
universe u

Lean source · statement

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

theorem

stwE5_sectionIdeal_comap

L81 ↗

AlgebraicGeometry.stwE5_sectionIdeal_comap

Source context 8 commands

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

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

Lean source · statement

theorem stwE5_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

stwE5_isInvertible_sectionIdeal

L99 ↗

AlgebraicGeometry.stwE5_isInvertible_sectionIdeal

Source context 8 commands

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

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

Lean source · statement

theorem stwE5_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