Module

AlgebraicPoints.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.AlgebraicPoints

47 declarations indexed from sourceView source ↗

Module documentation

Algebraic Points

Imports2

Imported by12

def

AlgPoints

L34 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints

Documentation

The group of algebra-valued points of the commutative relative group scheme in additive notation.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def AlgPoints (L : RelativeGroupLaw R f) (_hc : L.IsCommutative) (T : Type) [CommRing T]
    [Algebra R T] : Type

instance

instAddCommGroup

L43 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.instAddCommGroup

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

instance instAddCommGroup : AddCommGroup (L.AlgPoints hc T)

instance

instInhabited

L46 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.instInhabited

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

instance instInhabited : Inhabited (L.AlgPoints hc T)

def

ofPoint

L49 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint

Documentation

The algebra-valued point regarded as an element of the additive group of points.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

def ofPoint (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    L.AlgPoints hc T

def

toPoint

L53 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint

Documentation

The underlying scheme point of an element of the additive group of points.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

def toPoint (x : L.AlgPoints hc T) :
    SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f

theorem

toPoint_ofPoint

L56 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_ofPoint

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_ofPoint (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T)))
  f) :
    toPoint (ofPoint x : L.AlgPoints hc T) = x

theorem

ofPoint_toPoint

L60 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_toPoint

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_toPoint (x : L.AlgPoints hc T) : ofPoint (toPoint x) = x

theorem

toPoint_injective

L62 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_injective

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_injective : Function.Injective (toPoint : L.AlgPoints hc T → _)

theorem

ofPoint_injective

L65 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_injective

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_injective :
    Function.Injective (ofPoint : _ → L.AlgPoints hc T)

theorem

ext

L69 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ext

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ext {x y : L.AlgPoints hc T} (h : toPoint x = toPoint y) : x = y

def

equivPoint

L72 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.equivPoint

Documentation

The equivalence between the additive group of points and the underlying scheme points.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · full declaration

def equivPoint : L.AlgPoints hc T ≃ SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f
  where
  toFun := toPoint
  invFun := ofPoint
  left_inv _ := rfl
  right_inv _ := rfl

theorem

equivPoint_apply

L79 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.equivPoint_apply

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem equivPoint_apply (x : L.AlgPoints hc T) : equivPoint x = toPoint x

theorem

equivPoint_symm_apply

L81 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.equivPoint_symm_apply

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem equivPoint_symm_apply
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    (equivPoint.symm x : L.AlgPoints hc T) = ofPoint x

theorem

toPoint_add

L85 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_add

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_add (x y : L.AlgPoints hc T) :
    toPoint (x + y) = L.mul _ (toPoint x) (toPoint y)

theorem

toPoint_zero

L88 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_zero

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_zero : toPoint (0 : L.AlgPoints hc T) = L.one _

theorem

toPoint_neg

L90 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_neg

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_neg (x : L.AlgPoints hc T) : toPoint (-x) = L.inv _ (toPoint x)

theorem

ofPoint_mul

L92 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_mul

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_mul (x y : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    (ofPoint (L.mul _ x y) : L.AlgPoints hc T) = ofPoint x + ofPoint y

theorem

ofPoint_one

L95 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_one

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_one : (ofPoint (L.one _) : L.AlgPoints hc T) = 0

theorem

ofPoint_inv

L97 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_inv

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_inv (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    (ofPoint (L.inv _ x) : L.AlgPoints hc T) = -ofPoint x

theorem

toPoint_nsmul

L100 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_nsmul

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_nsmul (n : ℕ) (x : L.AlgPoints hc T) :
    toPoint (n • x) = L.nsmul _ n (toPoint x)

theorem

ofPoint_nsmul

L106 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.ofPoint_nsmul

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem ofPoint_nsmul (n : ℕ) (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f)
  :
    (ofPoint (L.nsmul _ n x) : L.AlgPoints hc T) = n • ofPoint x

theorem

toPoint_natCast_zsmul

L111 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_natCast_zsmul

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_natCast_zsmul (n : ℕ) (x : L.AlgPoints hc T) :
    toPoint ((n : ℤ) • x) = L.nsmul _ n (toPoint x)

theorem

nsmul_eq_zero_iff

L115 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.nsmul_eq_zero_iff

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem nsmul_eq_zero_iff (n : ℕ) (x : L.AlgPoints hc T) :
    n • x = 0 ↔ L.IsTorsionPoint _ n (toPoint x)

theorem

natCast_zsmul_eq_zero_iff

L120 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.natCast_zsmul_eq_zero_iff

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem natCast_zsmul_eq_zero_iff (n : ℕ) (x : L.AlgPoints hc T) :
    (n : ℤ) • x = 0 ↔ L.IsTorsionPoint _ n (toPoint x)

theorem

toPoint_mem_torsionSubset_iff

L124 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_mem_torsionSubset_iff

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_mem_torsionSubset_iff (n : ℕ) (x : L.AlgPoints hc T) :
    toPoint x ∈ L.torsionSubset _ n ↔ n • x = 0

theorem

mem_torsionBy_iff

L128 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.mem_torsionBy_iff

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem mem_torsionBy_iff (n : ℕ) (x : L.AlgPoints hc T) :
    x ∈ Submodule.torsionBy ℤ (L.AlgPoints hc T) (n : ℤ) ↔ L.IsTorsionPoint _ n (toPoint x)

def

torsionByEquiv

L135 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.torsionByEquiv

Documentation

The equivalence between the additive n-torsion submodule and the scheme-point torsion subset.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · full declaration

def torsionByEquiv (n : ℕ) :
    Submodule.torsionBy ℤ (L.AlgPoints hc T) (n : ℤ) ≃
      L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap R T))) n where
  toFun x := ⟨toPoint (x : L.AlgPoints hc T), (mem_torsionBy_iff n _).1 x.2⟩
  invFun y := ⟨ofPoint y.1, (mem_torsionBy_iff n _).2 y.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

theorem

torsionByEquiv_apply_coe

L143 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.torsionByEquiv_apply_coe

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem torsionByEquiv_apply_coe (n : ℕ)
    (x : Submodule.torsionBy ℤ (L.AlgPoints hc T) (n : ℤ)) :
    ((torsionByEquiv n x : L.torsionSubset _ n) : SchemeHomOver _ f) =
      toPoint (x : L.AlgPoints hc T)

theorem

torsionByEquiv_symm_apply_coe

L148 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.torsionByEquiv_symm_apply_coe

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem torsionByEquiv_symm_apply_coe (n : ℕ)
    (y : L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap R T))) n) :
    (((torsionByEquiv n).symm y : Submodule.torsionBy ℤ (L.AlgPoints hc T) (n : ℤ)) :
      L.AlgPoints hc T) = ofPoint y.1

theorem

natCard_torsionBy

L153 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.natCard_torsionBy

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem natCard_torsionBy (n : ℕ) :
    Nat.card (Submodule.torsionBy ℤ (L.AlgPoints hc T) (n : ℤ)) =
      Nat.card (L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap R T))) n)

theorem

specMap_comp_algebraMap

L162 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.specMap_comp_algebraMap

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem specMap_comp_algebraMap (a : T →ₐ[R] T') :
    Spec.map (CommRingCat.ofHom a.toRingHom) ≫ Spec.map (CommRingCat.ofHom (algebraMap R T)) =
      Spec.map (CommRingCat.ofHom (algebraMap R T'))

def

mapPoint

L170 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.mapPoint

Documentation

The point obtained by extending the coefficient algebra.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

def mapPoint (a : T →ₐ[R] T')
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T'))) f

theorem

mapPoint_coe

L176 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.mapPoint_coe

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem mapPoint_coe (a : T →ₐ[R] T')
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    (mapPoint a x).1 = Spec.map (CommRingCat.ofHom a.toRingHom) ≫ x.1

theorem

mapPoint_mul

L180 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.mapPoint_mul

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem mapPoint_mul (a : T →ₐ[R] T')
    (x y : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    mapPoint a (L.mul _ x y) = L.mul _ (mapPoint a x) (mapPoint a y)

theorem

mapPoint_one

L185 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.mapPoint_one

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem mapPoint_one (a : T →ₐ[R] T') :
    mapPoint (f := f) a (L.one _) = L.one _

def

map

L193 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.map

Documentation

The additive homomorphism on algebra-valued points induced by extension of the coefficient algebra.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

def map (a : T →ₐ[R] T') : L.AlgPoints hc T →+ L.AlgPoints hc T'

theorem

toPoint_map

L200 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_map

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem toPoint_map (a : T →ₐ[R] T') (x : L.AlgPoints hc T) :
    toPoint (map a x) = mapPoint a (toPoint x)

theorem

toPoint_map_coe

L203 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_map_coe

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem toPoint_map_coe (a : T →ₐ[R] T') (x : L.AlgPoints hc T) :
    (toPoint (map a x)).1 = Spec.map (CommRingCat.ofHom a.toRingHom) ≫ (toPoint x).1

theorem

map_ofPoint

L206 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.map_ofPoint

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem map_ofPoint (a : T →ₐ[R] T')
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    map a (ofPoint x : L.AlgPoints hc T) = ofPoint (mapPoint a x)

theorem

map_id

L210 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.map_id

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem map_id : map (AlgHom.id R T) = AddMonoidHom.id (L.AlgPoints hc T)

theorem

map_comp

L218 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.map_comp

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem map_comp (a : T →ₐ[R] T') (b : T' →ₐ[R] T'') :
    map (b.comp a) = (map b).comp (map a : L.AlgPoints hc T →+ L.AlgPoints hc T')

theorem

isTorsionPoint_toPoint_map

L225 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.isTorsionPoint_toPoint_map

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]
section Map
variable {T' : Type} [CommRing T'] [Algebra R T'] {T'' : Type} [CommRing T''] [Algebra R T'']

Lean source · statement

theorem isTorsionPoint_toPoint_map (a : T →ₐ[R] T') (n : ℕ) {x : L.AlgPoints hc T}
    (hx : L.IsTorsionPoint _ n (toPoint x)) : L.IsTorsionPoint _ n (toPoint (map a x))

instance

instDistribMulAction

L232 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.instDistribMulAction

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · full declaration

instance instDistribMulAction : DistribMulAction (T ≃ₐ[R] T) (L.AlgPoints hc T) where
  smul σ x := map (σ : T →ₐ[R] T) x
  one_smul x := by
    change map ((1 : T ≃ₐ[R] T) : T →ₐ[R] T) x = x
    rw [show ((1 : T ≃ₐ[R] T) : T →ₐ[R] T) = AlgHom.id R T from rfl, map_id]
    rfl
  mul_smul σ τ x := by
    change map ((σ * τ : T ≃ₐ[R] T) : T →ₐ[R] T) x = map (σ : T →ₐ[R] T) (map (τ : T →ₐ[R] T) x)
    rw [show ((σ * τ : T ≃ₐ[R] T) : T →ₐ[R] T) = (σ : T →ₐ[R] T).comp (τ : T →ₐ[R] T) from rfl,
      map_comp]
    rfl
  smul_zero σ := map_zero _
  smul_add σ x y := map_add _ x y

theorem

smul_def

L246 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.smul_def

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem smul_def (σ : T ≃ₐ[R] T) (x : L.AlgPoints hc T) : σ • x = map (σ : T →ₐ[R] T) x

theorem

toPoint_smul_coe

L248 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.toPoint_smul_coe

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem toPoint_smul_coe (σ : T ≃ₐ[R] T) (x : L.AlgPoints hc T) :
    (toPoint (σ • x)).1 = Spec.map (CommRingCat.ofHom (σ : T →ₐ[R] T).toRingHom) ≫ (toPoint x).1

theorem

smul_ofPoint

L252 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.smul_ofPoint

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem smul_ofPoint (σ : T ≃ₐ[R] T)
    (x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R T))) f) :
    σ • (ofPoint x : L.AlgPoints hc T) = ofPoint (mapPoint (σ : T →ₐ[R] T) x)

theorem

nsmul_smul_eq_zero

L256 ↗

GoodReductionJacobian.RelativeGroupLaw.AlgPoints.nsmul_smul_eq_zero

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
variable {R : Type} [CommRing R] {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of R)}
namespace AlgPoints
variable {L : RelativeGroupLaw R f} {hc : L.IsCommutative}
variable {T : Type} [CommRing T] [Algebra R T]

Lean source · statement

theorem nsmul_smul_eq_zero (σ : T ≃ₐ[R] T) (n : ℕ) {x : L.AlgPoints hc T} (hx : n • x = 0) :
    n • (σ • x) = 0

Module documentation

Algebraic Points

Declarations