Module

UnpointedComparisonHom.lean

Nyll.JacobianVarieties.Picard.UnpointedComparisonHom

4 declarations indexed from sourceView source ↗

Module documentation

The pointed comparison preserves the actual relative group laws

Imports3

Imported by1

Nyll.JacobianVarieties.Picard.All

theorem

pointedUnrigidifiedRepresentation_mul

L31 ↗

JacobianVarieties.Picard.Unpointed.pointedUnrigidifiedRepresentation_mul

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
open scoped CategoryTheory.MonObj
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)

Lean source · statement

theorem pointedUnrigidifiedRepresentation_mul {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (x y : SchemeHomOver t D.toBase) :
    (pointedUnrigidifiedRepresentation ε h).homEquiv
        (schemeHomOverToOverHom
          ((h.relativeGroupLaw (P := algEquivZeroGroupCut c ε)).mul t x y)) =
      Unrigidified.zeroMul (op (Over.mk t))
        ((pointedUnrigidifiedRepresentation ε h).homEquiv (schemeHomOverToOverHom x))
        ((pointedUnrigidifiedRepresentation ε h).homEquiv (schemeHomOverToOverHom y))

def

pointedComparisonPoint

L61 ↗

JacobianVarieties.Picard.Unpointed.pointedComparisonPoint

Documentation

Postcomposition with the actual pointed comparison on relative points.

Source context 8 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
open scoped CategoryTheory.MonObj
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]

Lean source · statement

def pointedComparisonPoint {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K))
    (x : SchemeHomOver t (toBase K c)) : SchemeHomOver t D.toBase

theorem

pointedComparisonPoint_classes

L67 ↗

JacobianVarieties.Picard.Unpointed.pointedComparisonPoint_classes

Source context 8 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
open scoped CategoryTheory.MonObj
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]

Lean source · statement

theorem pointedComparisonPoint_classes {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (x : SchemeHomOver t (toBase K c)) :
    (pointedUnrigidifiedRepresentation ε h).homEquiv
        (schemeHomOverToOverHom (pointedComparisonPoint c ε h t x)) =
      ((presentation K c).pointedRepresentation ε h).homEquiv (schemeHomOverToOverHom x)

theorem

pointedComparison_mul

L75 ↗

JacobianVarieties.Picard.Unpointed.pointedComparison_mul

Documentation

The scheme comparison preserves multiplication for every test scheme.

Source context 8 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
open scoped CategoryTheory.MonObj
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
  {D : RelativePic0Designation K c}
  (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]

Lean source · statement

theorem pointedComparison_mul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K))
    (x y : SchemeHomOver t (toBase K c)) :
    pointedComparisonPoint c ε h t ((groupLaw K c).mul t x y) =
      (h.relativeGroupLaw (P := algEquivZeroGroupCut c ε)).mul t
        (pointedComparisonPoint c ε h t x) (pointedComparisonPoint c ε h t y)

Module documentation

The pointed comparison preserves the actual relative group laws

Declarations

pointedUnrigidifiedRepresentation_mul

pointedComparisonPoint

pointedComparisonPoint_classes

pointedComparison_mul