Module

RepresentsRelSubPic_postComp_mul_of_classify_rel.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_postComp_mul_of_classify_rel

3 declarations indexed from sourceView source ↗

Module documentation

Multiplication compatibility from a relation on line bundles

A tensor-compatible relation on rigidified line bundles makes the associated morphism between representing schemes preserve multiplication of points.

Imports5

Imported by3

theorem

homEquiv_coe

L50 ↗

JacobianVarieties.Picard.Proofs.RepresentsRelSubPic_postComp_mul_of_classify_rel.H1.homEquiv_coe

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RepresentsRelSubPic_postComp_mul_of_classify_rel
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
open scoped CategoryTheory.MonObj
noncomputable section
namespace H1
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}

Lean source · statement

theorem homEquiv_coe (h : RepresentsRelSubPic c ε P.toSubPicCondition D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (g : Over.mk t ⟶ Over.mk D.toBase) :
    (h.representableBy.homEquiv g).1 =
      Quotient.mk _ (h.poincare.pullbackAlong ⟨g.left, Over.w g⟩)

theorem

mul_classify

L56 ↗

JacobianVarieties.Picard.Proofs.RepresentsRelSubPic_postComp_mul_of_classify_rel.H1.mul_classify

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RepresentsRelSubPic_postComp_mul_of_classify_rel
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
open scoped CategoryTheory.MonObj
noncomputable section
namespace H1
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}

Lean source · statement

theorem mul_classify (h : RepresentsRelSubPic c ε P.toSubPicCondition D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (M₁ M₂ : RigidifiedLineBundle c ε t) (h₁ : P.P t M₁) (h₂ : P.P t M₂) :
    h.relativeGroupLaw.mul t (h.classify t M₁ h₁) (h.classify t M₂ h₂)
      = h.classify t (M₁.tensor M₂) (P.tensor_mem t M₁ M₂ h₁ h₂)

theorem

postComp_mul_of_classify_rel

L89 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.postComp_mul_of_classify_rel

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RepresentsRelSubPic_postComp_mul_of_classify_rel
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
open scoped CategoryTheory.MonObj

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.postComp_mul_of_classify_rel
    {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 : SubPicGroupCondition c ε} {P' : SubPicGroupCondition c' ε'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D)
    (h' : RepresentsRelSubPic c' ε' P'.toSubPicCondition D')
    (θ : SchemeHomOver D.toBase D'.toBase)
    (Rel : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
      RigidifiedLineBundle c ε t → RigidifiedLineBundle c' ε' t → Prop)
    (hθ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
        (M : RigidifiedLineBundle c ε t) (hM : P.P t M)
        (N : RigidifiedLineBundle c' ε' t) (hN : P'.P t N),
      Rel t M N → postComp θ (h.classify t M hM) = h'.classify t N hN)
    (htotal : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
      (M : RigidifiedLineBundle c ε t), P.P t M →
      ∃ N : RigidifiedLineBundle c' ε' t, P'.P t N ∧ Rel t M N)
    (htensor : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
        (M₁ M₂ : RigidifiedLineBundle c ε t) (N₁ N₂ : RigidifiedLineBundle c' ε' t),
      Rel t M₁ N₁ → Rel t M₂ N₂ → Rel t (M₁.tensor M₂) (N₁.tensor N₂)) :
    ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t D.toBase),
      postComp θ (h.relativeGroupLaw.mul t x y) =
        h'.relativeGroupLaw.mul t (postComp θ x) (postComp θ y)

Module documentation

Multiplication compatibility from a relation on line bundles

Declarations

homEquiv_coe

mul_classify

postComp_mul_of_classify_rel