Module

Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback

26 declarations indexed from sourceView source ↗

Module documentation

Polarisation loc Iso On Base faces pullback cube iff of is Pullback

Imports6

Imported by2

theorem

locIsoOnBase_of_iso

L49 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.locIsoOnBase_of_iso

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section lociso
variable {S' : Type} [CommRing S'] {X Y Z : Scheme.{0}}

Lean source · statement

theorem locIsoOnBase_of_iso (q : X ⟶ Spec (CommRingCat.of S')) {M M' : X.Modules} (e : M ≅ M') :
  LocIsoOnBase q M M'

theorem

locIsoOnBase_unit_congr

L53 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.locIsoOnBase_unit_congr

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section lociso
variable {S' : Type} [CommRing S'] {X Y Z : Scheme.{0}}

Lean source · statement

theorem locIsoOnBase_unit_congr (q : X ⟶ Spec (CommRingCat.of S')) {M M' : X.Modules} (e : M ≅ M') :
    LocIsoOnBase q M (𝟙_ _) ↔ LocIsoOnBase q M' (𝟙_ _)

def

pullbackCompCongr

L59 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.pullbackCompCongr

Documentation

The comparison isomorphism between iterated pullback and pullback along an equal composite.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section lociso
variable {S' : Type} [CommRing S'] {X Y Z : Scheme.{0}}

Lean source · statement

def pullbackCompCongr {φ : X ⟶ Y} {ψ : Y ⟶ Z} {χ : X ⟶ Z} (h : φ ≫ ψ = χ) (M : Z.Modules) :
    (Scheme.Modules.pullback φ).obj ((Scheme.Modules.pullback ψ).obj M) ≅ (Scheme.Modules.pullback
      χ).obj M

theorem

locIsoOnBase_unit_iff_of_iso

L64 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.locIsoOnBase_unit_iff_of_iso

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section lociso
variable {S' : Type} [CommRing S'] {X Y Z : Scheme.{0}}

Lean source · statement

theorem locIsoOnBase_unit_iff_of_iso (e : X ≅ Y) (qX : X ⟶ Spec (CommRingCat.of S')) (qY : Y ⟶ Spec
  (CommRingCat.of S'))
    (he : e.hom ≫ qY = qX) (K : Y.Modules) :
    LocIsoOnBase qX ((Scheme.Modules.pullback e.hom).obj K) (𝟙_ _) ↔ LocIsoOnBase qY K (𝟙_ _)

theorem

one_coe_eq

L96 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.one_coe_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 one_coe_eq {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)) : (G.one t).1 = t ≫ (G.one (𝟙 _)).1

theorem

one_comp_a

L101 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.one_comp_a

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 one_comp_a {T : Scheme.{0}} (t : T ⟶ Spec (CommRingCat.of S)) :
    (L.one t).1 ≫ a = (L₁.one (t ≫ Spec.map (CommRingCat.ofHom φ))).1

def

aa

L118 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aa

Documentation

The morphism between the double fibre products induced by the given base change.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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

def aa : pullback f f ⟶ pullback f₁ f₁

theorem

aa_fst

L121 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aa_fst

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 aa_fst : aa φ a ha ≫ pullback.fst f₁ f₁ = pullback.fst f f ≫ a

theorem

aa_snd

L123 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aa_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 aa_snd : aa φ a ha ≫ pullback.snd f₁ f₁ = pullback.snd f f ≫ a

theorem

aa_prodStr

L126 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aa_prodStr

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 aa_prodStr : aa φ a ha ≫ prodStr f₁ f₁ = prodStr f f ≫ Spec.map (CommRingCat.ofHom φ)

def

aaa

L131 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aaa

Documentation

The morphism between the triple fibre products induced by the given base change.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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

def aaa : pullback (prodStr f f) f ⟶ pullback (prodStr f₁ f₁) f₁

theorem

aaa_fst

L146 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aaa_fst

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 aaa_fst : aaa φ a ha ≫ pullback.fst (prodStr f₁ f₁) f₁ = pullback.fst
  (prodStr f f) f ≫ aa φ a ha

theorem

aaa_snd

L149 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.aaa_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 aaa_snd : aaa φ a ha ≫ pullback.snd (prodStr f₁ f₁) f₁ = pullback.snd
  (prodStr f f) f ≫ a

def

θ

L157 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.θ

Documentation

The isomorphism identifying the double fibre product with the base change of the original double fibre product.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 · full declaration

def θ : pullback f f ≅ pullback (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom φ)) where
  hom := pullback.lift (aa φ a ha) (prodStr f f) (aa_prodStr φ a ha)
  inv := pullback.lift
    (ha.lift (pullback.fst _ _ ≫ pullback.fst f₁ f₁) (pullback.snd _ _)
      (by rw [Category.assoc]; exact pullback.condition))
    (ha.lift (pullback.fst _ _ ≫ pullback.snd f₁ f₁) (pullback.snd _ _)
      (by rw [Category.assoc, pullback_snd_comp_eq_prodStr]; exact pullback.condition))
    (by rw [IsPullback.lift_snd, IsPullback.lift_snd])
  hom_inv_id := by
    apply pullback.hom_ext
    · rw [Category.assoc, pullback.lift_fst, Category.id_comp]
      apply ha.hom_ext
      · rw [Category.assoc, IsPullback.lift_fst, pullback.lift_fst_assoc, aa_fst]
      · rw [Category.assoc, IsPullback.lift_snd, pullback.lift_snd]
    · rw [Category.assoc, pullback.lift_snd, Category.id_comp]
      apply ha.hom_ext
      · rw [Category.assoc, IsPullback.lift_fst, pullback.lift_fst_assoc, aa_snd]
      · rw [Category.assoc, IsPullback.lift_snd, pullback.lift_snd]; exact pullback.condition (f :=
          f) (g := f)
  inv_hom_id := by
    apply pullback.hom_ext
    · rw [Category.assoc, pullback.lift_fst, Category.id_comp]
      apply pullback.hom_ext
      · rw [Category.assoc, aa_fst, pullback.lift_fst_assoc, IsPullback.lift_fst]
      · rw [Category.assoc, aa_snd, pullback.lift_snd_assoc, IsPullback.lift_fst]
    · rw [Category.assoc, pullback.lift_snd, Category.id_comp]
      change _ ≫ pullback.fst f f ≫ f = _
      rw [pullback.lift_fst_assoc, IsPullback.lift_snd]

theorem

θ_hom_fst

L186 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.θ_hom_fst

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 θ_hom_fst : (θ φ a ha).hom ≫ pullback.fst _ _ = aa φ a ha

theorem

θ_hom_snd

L187 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.θ_hom_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 θ_hom_snd : (θ φ a ha).hom ≫ pullback.snd _ _ = prodStr f f

theorem

one_prodStr_comp_a

L189 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.one_prodStr_comp_a

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section square
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 one_prodStr_comp_a : (L.one (prodStr f f)).1 ≫ a = aa φ a ha ≫ (L₁.one (prodStr f₁ f₁)).1

def

F1

L210 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F1

Documentation

The first face map inserting the identity section as the first coordinate.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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

def F1 {R : Type} [CommRing R] {B : Scheme.{0}} {g : B ⟶ Spec (CommRingCat.of R)} (G :
  RelativeGroupLaw R g) :
    pullback g g ⟶ pullback (prodStr g g) g

def

F2

L219 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F2

Documentation

The second face map inserting the identity section as the second coordinate.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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

def F2 {R : Type} [CommRing R] {B : Scheme.{0}} {g : B ⟶ Spec (CommRingCat.of R)} (G :
  RelativeGroupLaw R g) :
    pullback g g ⟶ pullback (prodStr g g) g

def

F3

L228 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F3

Documentation

The third face map inserting the identity section as the third coordinate.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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

def F3 {R : Type} [CommRing R] {B : Scheme.{0}} {g : B ⟶ Spec (CommRingCat.of R)} (G :
  RelativeGroupLaw R g) :
    pullback g g ⟶ pullback (prodStr g g) g

theorem

F1_comp

L233 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F1_comp

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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 F1_comp : F1 L ≫ aaa φ a ha = aa φ a ha ≫ F1 L₁

theorem

F2_comp

L247 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F2_comp

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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 F2_comp : F2 L ≫ aaa φ a ha = aa φ a ha ≫ F2 L₁

theorem

F3_comp

L261 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.F3_comp

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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 F3_comp : F3 L ≫ aaa φ a ha = aa φ a ha ≫ F3 L₁

def

faceIso

L271 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.faceIso

Documentation

The pullback comparison for a face map compatible with the base-change morphisms.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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

def faceIso {F : pullback f f ⟶ pullback (prodStr f f) f} {F₁ : pullback f₁ f₁ ⟶ pullback (prodStr
  f₁ f₁) f₁}
    (hF : F ≫ aaa φ a ha = aa φ a ha ≫ F₁) (N : (pullback (prodStr f₁ f₁) f₁).Modules) :
    (Scheme.Modules.pullback F).obj ((Scheme.Modules.pullback (aaa φ a ha)).obj N) ≅
      (Scheme.Modules.pullback (θ φ a ha).hom).obj
        ((Scheme.Modules.pullback (pullback.fst (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom
          φ)))).obj
          ((Scheme.Modules.pullback F₁).obj N))

theorem

face_iff

L282 ↗

AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback.FBC.face_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
namespace FBC
open AlgebraicGeometry.Scheme.Modules
section faces
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)
omit hLa in

Lean source · statement

theorem face_iff {F : pullback f f ⟶ pullback (prodStr f f) f} {F₁ : pullback f₁ f₁ ⟶ pullback
  (prodStr f₁ f₁) f₁}
    (hF : F ≫ aaa φ a ha = aa φ a ha ≫ F₁) (N : (pullback (prodStr f₁ f₁) f₁).Modules) :
    LocIsoOnBase (prodStr f f) ((Scheme.Modules.pullback F).obj ((Scheme.Modules.pullback (aaa φ a
      ha)).obj N)) (𝟙_ _) ↔
      LocIsoOnBase (pullback.snd (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom φ)))
        ((Scheme.Modules.pullback (pullback.fst (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom
          φ)))).obj
          ((Scheme.Modules.pullback F₁).obj N)) (𝟙_ _)

theorem

locIsoOnBase_faces_pullback_cube_iff_of_isPullback

L305 ↗

AlgebraicGeometry.Polarisation.locIsoOnBase_faces_pullback_cube_iff_of_isPullback

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
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
noncomputable section
attribute [local simp] FBC.aa_fst
attribute [local simp] FBC.aa_snd
attribute [local simp] FBC.aaa_fst
attribute [local simp] FBC.aaa_snd
open FBC in

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Polarisation.locIsoOnBase_faces_pullback_cube_iff_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)
    (N : (pullback (prodStr f₁ f₁) f₁).Modules) :
    (LocIsoOnBase (prodStr f f)
        ((Scheme.Modules.pullback (pullback.lift
          (pullback.lift (L.one (prodStr f f)).1 (pullback.fst f f) (by rw [(L.one _).2]))
          (pullback.snd f f)
          (by rw [pullback.lift_fst_assoc, (L.one _).2]; exact pullback.condition))).obj
          ((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 N)) (𝟙_ _) ↔
      LocIsoOnBase (pullback.snd (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom φ)))
        ((Scheme.Modules.pullback (pullback.fst (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom
          φ)))).obj
          ((Scheme.Modules.pullback (pullback.lift
          (pullback.lift (L₁.one (prodStr f₁ f₁)).1 (pullback.fst f₁ f₁) (by rw [(L₁.one _).2]))
          (pullback.snd f₁ f₁)
          (by rw [pullback.lift_fst_assoc, (L₁.one _).2]; exact pullback.condition))).obj
          N)) (𝟙_ _)) ∧
    (LocIsoOnBase (prodStr f f)
        ((Scheme.Modules.pullback (pullback.lift
          (pullback.lift (pullback.fst f f) (L.one (prodStr f f)).1 (by rw [(L.one _).2]))
          (pullback.snd f f)
          (by rw [pullback.lift_fst_assoc]; exact pullback.condition))).obj
          ((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 N)) (𝟙_ _) ↔
      LocIsoOnBase (pullback.snd (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom φ)))
        ((Scheme.Modules.pullback (pullback.fst (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom
          φ)))).obj
          ((Scheme.Modules.pullback (pullback.lift
          (pullback.lift (pullback.fst f₁ f₁) (L₁.one (prodStr f₁ f₁)).1 (by rw [(L₁.one _).2]))
          (pullback.snd f₁ f₁)
          (by rw [pullback.lift_fst_assoc]; exact pullback.condition))).obj N)) (𝟙_ _)) ∧
    (LocIsoOnBase (prodStr f f)
        ((Scheme.Modules.pullback (pullback.lift (𝟙 _) (L.one (prodStr f f)).1
          (by rw [Category.id_comp, (L.one _).2]))).obj
          ((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 N)) (𝟙_ _) ↔
      LocIsoOnBase (pullback.snd (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom φ)))
        ((Scheme.Modules.pullback (pullback.fst (prodStr f₁ f₁) (Spec.map (CommRingCat.ofHom
          φ)))).obj
          ((Scheme.Modules.pullback (pullback.lift (𝟙 _) (L₁.one (prodStr f₁ f₁)).1
            (by rw [Category.id_comp, (L₁.one _).2]))).obj N)) (𝟙_ _)) := by
  exact ⟨FBC.face_iff φ a ha (FBC.F1_comp L₁ φ L a ha hLa) N,
    FBC.face_iff φ a ha (FBC.F2_comp L₁ φ L a ha hLa) N,
    FBC.face_iff φ a ha (FBC.F3_comp L₁ φ L a ha hLa) N⟩

Module documentation

Polarisation loc Iso On Base faces pullback cube iff of is Pullback

Declarations