Module

UnpointedPointedGroup.lean

Nyll.JacobianVarieties.Picard.UnpointedPointedGroup

6 declarations indexed from sourceView source ↗

Module documentation

Group compatibility of the pointed comparison

The comparison uses the descended universal element. Its effect on the identity and tensor products is determined by the actual classifying equivalences.

Imports4

Imported by3

theorem

homEquiv_uniqueUpToIso

L28 ↗

JacobianVarieties.Picard.Unpointed.homEquiv_uniqueUpToIso

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed

Lean source · statement

theorem homEquiv_uniqueUpToIso
    {S : Scheme.{u}} {F : (Over S)ᵒᵖ ⥤ Type (u + 1)}
    {A B T : Over S} (a : F.RepresentableBy A) (b : F.RepresentableBy B) (m : T ⟶ A) :
    b.homEquiv (m ≫ (a.uniqueUpToIso b).hom) = a.homEquiv m

theorem

pointedRepresentation_one

L41 ↗

JacobianVarieties.Picard.Unpointed.pointedRepresentation_one

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)

Lean source · statement

theorem pointedRepresentation_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) :
    ((presentation K c).pointedRepresentation ε h).homEquiv
        (schemeHomOverToOverHom ((groupLaw K c).one t)) =
      Unrigidified.zeroOne (c := c) (op (Over.mk t))

theorem

pointedRepresentation_mul

L58 ↗

JacobianVarieties.Picard.Unpointed.pointedRepresentation_mul

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)

Lean source · statement

theorem pointedRepresentation_mul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K))
    (x y : SchemeHomOver t (toBase K c)) :
    ((presentation K c).pointedRepresentation ε h).homEquiv
        (schemeHomOverToOverHom ((groupLaw K c).mul t x y)) =
      Unrigidified.zeroMul (op (Over.mk t))
        (((presentation K c).pointedRepresentation ε h).homEquiv (schemeHomOverToOverHom x))
        (((presentation K c).pointedRepresentation ε h).homEquiv (schemeHomOverToOverHom y))

theorem

pointedUnrigidifiedRepresentation_zero

L79 ↗

JacobianVarieties.Picard.Unpointed.pointedUnrigidifiedRepresentation_zero

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
omit [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c] in

Lean source · statement

theorem pointedUnrigidifiedRepresentation_zero :
    (pointedUnrigidifiedRepresentation ε h).homEquiv
        (Over.homMk D.zeroSection D.zeroSection_toBase) =
      Unrigidified.zeroOne (c := c) (op (Over.mk (𝟙 (Spec (CommRingCat.of K)))))

theorem

pointedComparison_classes

L86 ↗

JacobianVarieties.Picard.Unpointed.pointedComparison_classes

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)

Lean source · statement

theorem pointedComparison_classes {T : Over (Spec (CommRingCat.of K))}
    (m : T ⟶ Over.mk (toBase K c)) :
    (pointedUnrigidifiedRepresentation ε h).homEquiv
        (m ≫ ((presentation K c).pointedComparisonOver ε h).hom) =
      ((presentation K c).pointedRepresentation ε h).homEquiv m

theorem

pointedComparison_zero

L95 ↗

JacobianVarieties.Picard.Unpointed.pointedComparison_zero

Documentation

The actual pointed comparison sends the chosen unpointed identity to the zero section of the pointed Picard representative.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)

Lean source · statement

theorem pointedComparison_zero :
    ((groupLaw K c).one (𝟙 (Spec (CommRingCat.of K)))).1 ≫
        (pointedComparison c ε h).hom = D.zeroSection

Module documentation

Group compatibility of the pointed comparison

Declarations

homEquiv_uniqueUpToIso

pointedRepresentation_one

pointedRepresentation_mul

pointedUnrigidifiedRepresentation_zero

pointedComparison_classes

pointedComparison_zero