NYLL
Module

RigidifiedLineBundle_exists_rigidified_cube_pullback_of_isPullback.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_rigidified_cube_pullback_of_isPullback
6 declarations indexed from sourceView source ↗

Module documentation

Pullback of a rigidified line bundle on a triple product

A base-change square compatible with multiplication also preserves the unit section. The induced map on triple products therefore pulls back both the line bundle and its rigidification along the cube section.

Imports4
Imported by2

Declarations

theorem

eq_one_of_mul_self

L53 ↗
JacobianVarieties.Picard.Proofs.CubePullback.CubeRigBC.eq_one_of_mul_self
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace CubeRigBC
variable {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
  {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
  {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
  {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
  (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
  (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
    (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
      ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
      ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
Lean source · statement
theorem eq_one_of_mul_self {R : Type} [CommRing R] {B : Scheme.{0}}
    {g : B ⟶ Spec (CommRingCat.of R)} (G : RelativeGroupLaw R g)
    {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t g)
    (hx : G.mul t x x = x) : x = G.one t
theorem

one_comp

L61 ↗
JacobianVarieties.Picard.Proofs.CubePullback.CubeRigBC.one_comp
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace CubeRigBC
variable {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
  {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
  {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
  {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
  (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
  (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
    (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
      ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
      ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
include ha hLa in
Lean source · statement
theorem one_comp {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of S)) :
    (L.one t).1 ≫ a = (L₁.one (t ≫ Spec.map (CommRingCat.ofHom φ))).1
theorem

f_one_a

L71 ↗
JacobianVarieties.Picard.Proofs.CubePullback.CubeRigBC.f_one_a
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace CubeRigBC
variable {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
  {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
  {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
  {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
  (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
  (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
    (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
      ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
      ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
include ha hLa in
Lean source · statement
theorem f_one_a : f ≫ (L.one (𝟙 (Spec (CommRingCat.of S)))).1 ≫ a =
    a ≫ f₁ ≫ (L₁.one (𝟙 (Spec (CommRingCat.of S₁)))).1
abbrev

a3

L84 ↗
JacobianVarieties.Picard.Proofs.CubePullback.CubeRigBC.a3
Documentation

The map on triple fibre products induced by the given base-change square.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace CubeRigBC
variable {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
  {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
  {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
  {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
  (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
  (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
    (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
      ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
      ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
Lean source · statement
abbrev a3 : pullback (prodStr f f) f ⟶ pullback (prodStr f₁ f₁) f₁
theorem

rigSection_comp_a3

L99 ↗
JacobianVarieties.Picard.Proofs.CubePullback.CubeRigBC.rigSection_comp_a3
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
namespace CubeRigBC
variable {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
  {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
  {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
  {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
  (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
  (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
    (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
      ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
      ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
include hLa in
Lean source · statement
theorem rigSection_comp_a3 :
    rigSection (prodStr f f) f ((L.prod L).one (𝟙 (Spec (CommRingCat.of S)))) ≫ a3 φ a ha =
      a ≫ rigSection (prodStr f₁ f₁) f₁ ((L₁.prod L₁).one (𝟙 (Spec (CommRingCat.of S₁))))
theorem

exists_rigidified_cube_pullback_of_isPullback

L124 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.exists_rigidified_cube_pullback_of_isPullback
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.CubePullback
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
open CubeRigBC in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle
Lean source · full declaration
theorem exists_rigidified_cube_pullback_of_isPullback
    {S₁ : Type} [CommRing S₁] {A₁ : Scheme.{0}}
    {f₁ : A₁ ⟶ Spec (CommRingCat.of S₁)} (L₁ : RelativeGroupLaw S₁ f₁)
    {S : Type} [CommRing S] (φ : S₁ →+* S) {A : Scheme.{0}}
    {f : A ⟶ Spec (CommRingCat.of S)} (L : RelativeGroupLaw S f)
    (a : A ⟶ A₁) (ha : IsPullback a f f₁ (Spec.map (CommRingCat.ofHom φ)))
    (hLa : ∀ (T : Scheme.{0}) (t : T ⟶ Spec (CommRingCat.of S)) (P Q : SchemeHomOver t f),
      (L.mul t P Q).1 ≫ a = (L₁.mul (t ≫ Spec.map (CommRingCat.ofHom φ))
        ⟨P.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, P.2]⟩
        ⟨Q.1 ≫ a, by rw [Category.assoc, ha.w, ← Category.assoc, Q.2]⟩).1)
    (M₁ : RigidifiedLineBundle (prodStr f₁ f₁)
      ((L₁.prod L₁).one (𝟙 (Spec (CommRingCat.of S₁)))) f₁) :
    ∃ M : RigidifiedLineBundle (prodStr f f) ((L.prod L).one (𝟙 (Spec (CommRingCat.of S)))) f,
      M.L = (Scheme.Modules.pullback (pullback.map (prodStr f f) f (prodStr f₁ f₁) f₁
          (pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom φ)) ha.w.symm ha.w.symm)
          a (Spec.map (CommRingCat.ofHom φ))
          (by
            have h1 :
              pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom φ)) ha.w.symm ha.w.symm ≫
                pullback.fst f₁ f₁ = pullback.fst f f ≫ a := pullback.lift_fst _ _ _
            change (pullback.fst f f ≫ f) ≫ Spec.map (CommRingCat.ofHom φ) =
              pullback.map f f f₁ f₁ a a (Spec.map (CommRingCat.ofHom φ)) ha.w.symm ha.w.symm ≫
                pullback.fst f₁ f₁ ≫ f₁
            rw [Category.assoc, ← Category.assoc (pullback.map _ _ _ _ _ _ _ _ _),
              h1, Category.assoc, ha.w])
          ha.w.symm)).obj M₁.L :=
  ⟨{ L := (Scheme.Modules.pullback (a3 φ a ha)).obj M₁.L
     isInvertible := M₁.isInvertible.pullback _
     rigidified := ⟨(Scheme.Modules.pullbackComp _ _).app M₁.L ≪≫
        (Scheme.Modules.pullbackCongr (rigSection_comp_a3 L₁ φ L a ha hLa)).app M₁.L ≪≫
        ((Scheme.Modules.pullbackComp _ _).app M₁.L).symm ≪≫
        (Scheme.Modules.pullback a).mapIso M₁.rigidified.some ≪≫
        Scheme.Modules.pullbackUnitIso a⟩ }, rfl⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.