NYLL
Module

RepresentsRelSubPic_existsUnique_hom_of_transform.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_existsUnique_hom_of_transform
5 declarations indexed from sourceView source ↗

Module documentation

Morphisms induced by transformations of rigidified line bundles

A transformation compatible with isomorphisms and pullback induces a unique morphism between the schemes representing the two sub-Picard functors.

Imports5
Imported by8

Declarations

def

transformHom

L63 ↗
JacobianVarieties.Picard.Proofs.Transform.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.transformHom
Documentation

The morphism classifying the transformed universal rigidified line bundle.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Transform
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {P : SubPicCondition c ε} {P' : SubPicCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P D) (h' : RepresentsRelSubPic c' ε' P' D')
    (Φ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c' ε' t → RigidifiedLineBundle c ε t)
    (hcut : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t),
      P'.P t M → P.P t (Φ t M))
Lean source · statement
def transformHom : SchemeHomOver D'.toBase D.toBase
theorem

postComp_transformHom_classify

L76 ↗
JacobianVarieties.Picard.Proofs.Transform.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.postComp_transformHom_classify
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Transform
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {P : SubPicCondition c ε} {P' : SubPicCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P D) (h' : RepresentsRelSubPic c' ε' P' D')
    (Φ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c' ε' t → RigidifiedLineBundle c ε t)
    (hcut : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t),
      P'.P t M → P.P t (Φ t M))
variable
    (hcongr : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
      (M M' : RigidifiedLineBundle c' ε' t),
      Nonempty (M.L ≅ M'.L) → Nonempty ((Φ t M).L ≅ (Φ t M').L))
    (hnat : ∀ {T T' : Scheme.{u}}
      {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
      (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c' ε' t),
      Nonempty (((Φ t M).pullbackAlong ψ).L ≅ (Φ t' (M.pullbackAlong ψ)).L))
include hcongr hnat in
Lean source · statement
theorem postComp_transformHom_classify {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c' ε' t) (hM : P'.P t M) :
    postComp (transformHom h h' Φ hcut) (h'.classify t M hM) =
      h.classify t (Φ t M) (hcut t M hM)
theorem

transformHom_unique

L86 ↗
JacobianVarieties.Picard.Proofs.Transform.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.transformHom_unique
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Transform
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {P : SubPicCondition c ε} {P' : SubPicCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P D) (h' : RepresentsRelSubPic c' ε' P' D')
    (Φ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c' ε' t → RigidifiedLineBundle c ε t)
    (hcut : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t),
      P'.P t M → P.P t (Φ t M))
variable
    (hcongr : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
      (M M' : RigidifiedLineBundle c' ε' t),
      Nonempty (M.L ≅ M'.L) → Nonempty ((Φ t M).L ≅ (Φ t M').L))
    (hnat : ∀ {T T' : Scheme.{u}}
      {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
      (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c' ε' t),
      Nonempty (((Φ t M).pullbackAlong ψ).L ≅ (Φ t' (M.pullbackAlong ψ)).L))
Lean source · statement
theorem transformHom_unique (g : SchemeHomOver D'.toBase D.toBase)
    (hg : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t)
      (hM : P'.P t M), postComp g (h'.classify t M hM) = h.classify t (Φ t M) (hcut t M hM)) :
    g = transformHom h h' Φ hcut
theorem

existsUnique_hom_of_transform'

L99 ↗
JacobianVarieties.Picard.Proofs.Transform.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.existsUnique_hom_of_transform'
Source context 21 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Transform
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {P : SubPicCondition c ε} {P' : SubPicCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P D) (h' : RepresentsRelSubPic c' ε' P' D')
    (Φ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c' ε' t → RigidifiedLineBundle c ε t)
    (hcut : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t),
      P'.P t M → P.P t (Φ t M))
variable
    (hcongr : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
      (M M' : RigidifiedLineBundle c' ε' t),
      Nonempty (M.L ≅ M'.L) → Nonempty ((Φ t M).L ≅ (Φ t M').L))
    (hnat : ∀ {T T' : Scheme.{u}}
      {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
      (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c' ε' t),
      Nonempty (((Φ t M).pullbackAlong ψ).L ≅ (Φ t' (M.pullbackAlong ψ)).L))
include hcongr hnat in
Lean source · statement
theorem existsUnique_hom_of_transform' :
    ∃! φ : SchemeHomOver D'.toBase D.toBase,
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t)
        (hM : P'.P t M),
        postComp φ (h'.classify t M hM) = h.classify t (Φ t M) (hcut t M hM)
theorem

existsUnique_hom_of_transform

L112 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.existsUnique_hom_of_transform
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Transform
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
open _root_.AlgebraicGeometry.RelPicard in
open _root_.JacobianVarieties.Picard.Proofs.Transform.AlgebraicGeometry.RelPicard in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.existsUnique_hom_of_transform
    {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {P : SubPicCondition c ε} {P' : SubPicCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P D) (h' : RepresentsRelSubPic c' ε' P' D')
    (Φ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c' ε' t → RigidifiedLineBundle c ε t)
    (hcongr : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
      (M M' : RigidifiedLineBundle c' ε' t),
      Nonempty (M.L ≅ M'.L) → Nonempty ((Φ t M).L ≅ (Φ t M').L))
    (hnat : ∀ {T T' : Scheme.{u}}
      {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
      (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c' ε' t),
      Nonempty (((Φ t M).pullbackAlong ψ).L ≅ (Φ t' (M.pullbackAlong ψ)).L))
    (hcut : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t),
      P'.P t M → P.P t (Φ t M)) :
    ∃! φ : SchemeHomOver D'.toBase D.toBase,
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c' ε' t)
        (hM : P'.P t M),
        postComp φ (h'.classify t M hM) = h.classify t (Φ t M) (hcut t M hM)

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