Module

RepresentsRelSubPicGroup.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPicGroup

8 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Transport the group structure of a relative Picard presheaf to its representing designation.

Imports11

Imported by75

def

grpRepresentableBy

L48 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.grpRepresentableBy

Documentation

The representing bijection for the group-valued relative sub-Picard presheaf after forgetting its group structure.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · full declaration

def RepresentsRelSubPic.grpRepresentableBy {P : SubPicGroupCondition c ε} {D :
  RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) :
    ((relSubPicCommGrpPresheaf c ε P ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).RepresentableBy
      (Over.mk D.toBase) where
  homEquiv := h.representableBy.homEquiv
  homEquiv_comp f g := h.representableBy.homEquiv_comp f g

def

grpObj

L59 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.grpObj

Documentation

The group object on the representing scheme induced by the relative sub-Picard group presheaf.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def RepresentsRelSubPic.grpObj {P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) : GrpObj (Over.mk D.toBase)

def

relativeGroupLaw

L67 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.relativeGroupLaw

Documentation

The relative group law attached to the induced group object on the representing designation.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def RepresentsRelSubPic.relativeGroupLaw {P : SubPicGroupCondition c ε} {D :
  RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) : RelativeGroupLaw R D.toBase

theorem

homEquiv_mul

L73 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.homEquiv_mul

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · full declaration

theorem RepresentsRelSubPic.homEquiv_mul {P : SubPicGroupCondition c ε} {D :
  RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) (T : Over (Spec (CommRingCat.of R)))
    (a b : T ⟶ Over.mk D.toBase) :
    let _ : GrpObj (Over.mk D.toBase) := h.grpObj
    let _ : CommGroup
        ((relSubPicPresheaf c ε P.toSubPicCondition).obj (Opposite.op T)) :=
      P.commGroupObj (Opposite.op T)
    h.representableBy.homEquiv (a * b) = h.representableBy.homEquiv a *
      h.representableBy.homEquiv b := by
  intro groupObject pointGroup
  let := P.commGroupObj (Opposite.op (Over.mk D.toBase ⊗ Over.mk D.toBase))
  have hμ := MonObj.ofRepresentableBy_mul (Over.mk D.toBase)
    ((relSubPicCommGrpPresheaf c ε P ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget₂ GrpCat MonCat)
      h.grpRepresentableBy
  have hμ' : h.representableBy.homEquiv (μ[Over.mk D.toBase]) =
      h.representableBy.homEquiv (CartesianMonoidalCategory.fst (Over.mk D.toBase)
        (Over.mk D.toBase)) *
        h.representableBy.homEquiv (CartesianMonoidalCategory.snd (Over.mk D.toBase)
          (Over.mk D.toBase)) := by
    conv_lhs => rw [hμ]
    exact Equiv.apply_symm_apply _ _
  rw [Hom.mul_def, h.representableBy.homEquiv_comp, hμ']
  change ((relSubPicCommGrpPresheaf c ε P).map (CartesianMonoidalCategory.lift a b).op).hom
    (_ * _) = _
  erw [map_mul]
  change (relSubPicPresheaf c ε P.toSubPicCondition).map _ (h.representableBy.homEquiv _) *
      (relSubPicPresheaf c ε P.toSubPicCondition).map _ (h.representableBy.homEquiv _) = _
  rw [← h.representableBy.homEquiv_comp, ← h.representableBy.homEquiv_comp,
    CartesianMonoidalCategory.lift_fst, CartesianMonoidalCategory.lift_snd]
  rfl

theorem

homEquiv_one

L105 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.homEquiv_one

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · full declaration

theorem RepresentsRelSubPic.homEquiv_one {P : SubPicGroupCondition c ε} {D :
  RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) (T : Over (Spec (CommRingCat.of R))) :
    let _ : GrpObj (Over.mk D.toBase) := h.grpObj
    let _ : CommGroup
        ((relSubPicPresheaf c ε P.toSubPicCondition).obj (Opposite.op T)) :=
      P.commGroupObj (Opposite.op T)
    h.representableBy.homEquiv (1 : T ⟶ Over.mk D.toBase) = 1 := by
  intro groupObject pointGroup
  let := P.commGroupObj (Opposite.op (𝟙_ (Over (Spec (CommRingCat.of R)))))
  have hη := MonObj.ofRepresentableBy_one (Over.mk D.toBase)
    ((relSubPicCommGrpPresheaf c ε P ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget₂ GrpCat MonCat)
      h.grpRepresentableBy
  have hη' : h.representableBy.homEquiv (η[Over.mk D.toBase]) = 1 := by
    conv_lhs => rw [hη]
    exact Equiv.apply_symm_apply _ _
  rw [Hom.one_def, h.representableBy.homEquiv_comp, hη']
  change ((relSubPicCommGrpPresheaf c ε P).map (CartesianMonoidalCategory.toUnit T).op).hom 1 = 1
  exact map_one _

theorem

isCommMonObj

L125 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.isCommMonObj

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · full declaration

theorem RepresentsRelSubPic.isCommMonObj {P : SubPicGroupCondition c ε} {D :
  RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) :
    let _ : GrpObj (Over.mk D.toBase) := h.grpObj
    IsCommMonObj (Over.mk D.toBase) := by
  intro groupObject
  rw [isCommMonObj_iff_isMulCommutative]
  intro T
  let := P.commGroupObj (Opposite.op T)
  refine ⟨⟨fun a b => h.representableBy.homEquiv.injective ?_⟩⟩
  rw [h.homEquiv_mul, h.homEquiv_mul, mul_comm]

theorem

relativeGroupLaw_isCommutative

L137 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.relativeGroupLaw_isCommutative

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

theorem RepresentsRelSubPic.relativeGroupLaw_isCommutative {P : SubPicGroupCondition c ε}
    {D : RelativePic0Designation R c} (h : RepresentsRelSubPic c ε P.toSubPicCondition D) :
    h.relativeGroupLaw.IsCommutative

theorem

relativeGroupLaw_one

L144 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.relativeGroupLaw_one

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

theorem RepresentsRelSubPic.relativeGroupLaw_one {P : SubPicGroupCondition c ε}
    {D : RelativePic0Designation R c} (h : RepresentsRelSubPic c ε P.toSubPicCondition D) :
    (h.relativeGroupLaw.one (𝟙 _)).1 = D.zeroSection

Module documentation

Relative Picard varieties and fibre cohomology

Declarations