Module

Pic0_exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero.lean

Nyll.JacobianVarieties.Pic0.Pic0_exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero

81 declarations indexed from sourceView source ↗

Module documentation

Divisibility of Picard classes from a Jacobian presentation

A smooth proper connected Jacobian presentation gives division by an integer that is nonzero in the base field. The proof constructs multiplication morphisms, computes their cotangent maps using square-zero extensions, and deduces surjectivity from etaleness.

Imports16

Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.AlgClosed.Basic
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Stalk
Mathlib.Algebra.TrivSqZeroExt.Basic
Mathlib.RingTheory.Unramified.LocalRing
Mathlib.LinearAlgebra.Dual.Lemmas
Mathlib.Tactic.Algebraize
Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.Push
Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_of_field
Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_of_formallyUnramified_stalkMap
Nyll.AlgebraicCurves.Divisors.ClassGroup
Nyll.AlgebraicCurves.FunctionFields.CurveOver

Imported by3

theorem

surjective_of_universallyOpen_of_universallyClosed

L56 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.surjective_of_universallyOpen_of_universallyClosed

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem surjective_of_universallyOpen_of_universallyClosed
    {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversallyOpen f] [UniversallyClosed f]
    [Nonempty X] [PreconnectedSpace Y] : Surjective f

theorem

exists_comp_eq_of_surjective_of_isAlgClosed

L64 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.exists_comp_eq_of_surjective_of_isAlgClosed

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem exists_comp_eq_of_surjective_of_isAlgClosed
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Surjective f] [LocallyOfFiniteType f]
    {L : Type u} [Field L] [IsAlgClosed L] (p : Spec (.of L) ⟶ Y) :
    ∃ q : Spec (.of L) ⟶ X, q ≫ f = p

theorem

ext_of_forall_comp_eq_of_isAlgClosed

L78 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.ext_of_forall_comp_eq_of_isAlgClosed

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem ext_of_forall_comp_eq_of_isAlgClosed
    {K : Type u} [Field K] [IsAlgClosed K] {X Y Z : Scheme.{u}}
    (sX : X ⟶ Spec (.of K)) [LocallyOfFiniteType sX] [IsReduced X]
    {f g : X ⟶ Y} (sY : Y ⟶ Z) [IsSeparated sY] (hfg : f ≫ sY = g ≫ sY)
    (h : ∀ σ : Spec (.of K) ⟶ X, σ ≫ sX = 𝟙 _ → σ ≫ f = σ ≫ g) : f = g

theorem

comp_pullbackLift

L93 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.comp_pullbackLift

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · full declaration

theorem comp_pullbackLift {W X Y Z T : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z}
    (s : T ⟶ W) (a : W ⟶ X) (b : W ⟶ Y) (w : a ≫ f = b ≫ g) :
    s ≫ pullback.lift a b w =
      pullback.lift (s ≫ a) (s ≫ b) (by rw [Category.assoc, Category.assoc, w]) := by
  ext : 1 <;> simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd]

theorem

formallyUnramified_of_surjective_cotangent

L99 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.formallyUnramified_of_surjective_cotangent

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem JPHead.formallyUnramified_of_surjective_cotangent
    {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    [IsNoetherianRing S] (f : R →+* S) [IsLocalHom f] (hf : f.EssFiniteType)
    (hres : ∀ s : S, ∃ r : R, s - f r ∈ maximalIdeal S)
    (hcot : ∀ x ∈ maximalIdeal S, ∃ y ∈ maximalIdeal R, x - f y ∈ (maximalIdeal S) ^ 2) :
    f.FormallyUnramified

instance

(anonymous instance)

L138 ↗

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]

Lean source · statement

instance : IsLocalRing (TrivSqZeroExt K V)

theorem

isUnit_iff_fst_ne_zero

L149 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.TrivSqZeroExt.isUnit_iff_fst_ne_zero

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]

Lean source · statement

theorem TrivSqZeroExt.isUnit_iff_fst_ne_zero (a : TrivSqZeroExt K V) : IsUnit a ↔ a.fst ≠ 0

theorem

snd_nsmul'

L153 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.TrivSqZeroExt.snd_nsmul'

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
omit [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V] in

Lean source · statement

theorem TrivSqZeroExt.snd_nsmul' (n : ℕ) (z : TrivSqZeroExt K V) : (n • z).snd = n • z.snd

abbrev

Λ

L159 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λ

Documentation

The trivial square-zero extension, regarded as an object of CommRingCat.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]

Lean source · statement

abbrev Λ : CommRingCat.{u}

abbrev

Λmap

L165 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λmap

Documentation

The morphism of square-zero extensions induced by a linear map.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

abbrev Λmap (f : V →ₗ[K] W) : Λ K V ⟶ Λ K W

abbrev

Λfst

L169 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λfst

Documentation

The projection of the square-zero extension onto its coefficient field.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

abbrev Λfst : Λ K V ⟶ CommRingCat.of K

abbrev

Λinl

L173 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λinl

Documentation

The inclusion of the coefficient field in its square-zero extension.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

abbrev Λinl : CommRingCat.of K ⟶ Λ K V

instance

(anonymous instance)

L176 ↗

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

instance (f : V →ₗ[K] W) : IsLocalHom (Λmap f).hom

instance

(anonymous instance)

L183 ↗

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

instance : IsLocalHom (Λfst (K := K) (V := V)).hom

theorem

Λmap_id

L192 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λmap_id

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λmap_id : Λmap (LinearMap.id : V →ₗ[K] V) = 𝟙 _

theorem

Λmap_comp

L196 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λmap_comp

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λmap_comp (f : V →ₗ[K] W) (g : W →ₗ[K] P) : Λmap f ≫ Λmap g = Λmap (g ∘ₗ f)

theorem

Λmap_zero

L201 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λmap_zero

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λmap_zero : Λmap (0 : V →ₗ[K] W) = Λfst ≫ Λinl

theorem

Λmap_fst

L207 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λmap_fst

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λmap_fst (f : V →ₗ[K] W) : Λmap f ≫ Λfst = Λfst

theorem

Λinl_map

L212 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λinl_map

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λinl_map (f : V →ₗ[K] W) : Λinl ≫ Λmap f = Λinl

theorem

Λinl_fst

L217 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Λinl_fst

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section TSZE
variable (K : Type u) [Field K] (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V]
  [IsCentralScalar K V]
variable {K V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {P : Type u} [AddCommGroup P] [Module K P] [Module Kᵐᵒᵖ P] [IsCentralScalar K P]

Lean source · statement

theorem Λinl_fst : (Λinl : _ ⟶ Λ K V) ≫ Λfst = 𝟙 _

def

Φ

L228 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Φ

Documentation

The morphism to the scheme induced by a ring map from its stalk at the chosen point.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

def Φ {R : CommRingCat.{u}} (g : J.presheaf.stalk x₀ ⟶ R) : Spec R ⟶ J

theorem

Φ_comp

L231 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Φ_comp

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

theorem Φ_comp {R R' : CommRingCat.{u}} (g : J.presheaf.stalk x₀ ⟶ R) (φ : R ⟶ R') :
    Φ x₀ (g ≫ φ) = Spec.map φ ≫ Φ x₀ g

def

stalkEndo

L236 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.stalkEndo

Documentation

The stalk endomorphism induced by a scheme endomorphism fixing the chosen point.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

def stalkEndo (φ : J ⟶ J) (hφ : φ.base x₀ = x₀) :
    J.presheaf.stalk x₀ ⟶ J.presheaf.stalk x₀

theorem

Φ_comp_endo

L240 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Φ_comp_endo

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

theorem Φ_comp_endo {R : CommRingCat.{u}} (g : J.presheaf.stalk x₀ ⟶ R) (φ : J ⟶ J)
    (hφ : φ.base x₀ = x₀) : Φ x₀ g ≫ φ = Φ x₀ (stalkEndo x₀ φ hφ ≫ g)

theorem

Φ_injective

L246 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Φ_injective

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

theorem Φ_injective {R : CommRingCat.{u}} [IsLocalRing R] {g₁ g₂ : J.presheaf.stalk x₀ ⟶ R}
    [IsLocalHom g₁.hom] [IsLocalHom g₂.hom] (h : Φ x₀ g₁ = Φ x₀ g₂) : g₁ = g₂

theorem

exists_eq_Φ

L255 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.exists_eq_Φ

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)

Lean source · statement

theorem exists_eq_Φ {R : CommRingCat.{u}} [IsLocalRing R] (t : Spec R ⟶ J)
    (ht : t.base (closedPoint R) = x₀) :
    ∃ g : J.presheaf.stalk x₀ ⟶ R, IsLocalHom g.hom ∧ Φ x₀ g = t

def

ιO

L264 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.ιO

Documentation

The coefficient map to the chosen stalk, obtained from the structure morphism and the germ.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)
variable {K : Type u} [Field K] (c : J ⟶ Spec (.of K))

Lean source · statement

def ιO : CommRingCat.of K ⟶ J.presheaf.stalk x₀

theorem

Φ_comp_c

L267 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.Φ_comp_c

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Phi
variable {J : Scheme.{u}} (x₀ : J)
variable {K : Type u} [Field K] (c : J ⟶ Spec (.of K))

Lean source · statement

theorem Φ_comp_c {R : CommRingCat.{u}} (g : J.presheaf.stalk x₀ ⟶ R) :
    Φ x₀ g ≫ c = Spec.map (ιO x₀ c ≫ g)

theorem

mem_sq_ker_of_forall_snd_eq_zero

L280 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.mem_sq_ker_of_forall_snd_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Sep

Lean source · statement

theorem mem_sq_ker_of_forall_snd_eq_zero {O : Type u} [CommRing O] {K : Type u} [Field K]
    (ι : K →+* O) (ev : O →+* K) (hιev : ∀ a, ev (ι a) = a)
    (y : O) (hy : ev y = 0)
    (H : ∀ g : O →+* TrivSqZeroExt K K, (∀ x, (g x).fst = ev x) →
      (∀ a, g (ι a) = TrivSqZeroExt.inl a) → (g y).snd = 0) :
    y ∈ (RingHom.ker ev) ^ 2

def

nsmulHom

L373 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nsmulHom

Documentation

Repeated multiplication using the given multiplication morphism and identity section.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)

Lean source · full declaration

def nsmulHom : ℕ → {φ : J ⟶ J // φ ≫ c = c}
  | 0 => ⟨c ≫ e, by rw [Category.assoc, he, Category.comp_id]⟩
  | k + 1 => ⟨pullback.lift (nsmulHom k).1 (𝟙 J) (by rw [(nsmulHom k).2, Category.id_comp]) ≫ mul,
      by rw [Category.assoc, hmulK, pullback.lift_fst_assoc, (nsmulHom k).2]⟩

theorem

nsmulHom_zero

L378 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nsmulHom_zero

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)

Lean source · statement

theorem nsmulHom_zero : (nsmulHom c mul hmulK e he 0).1 = c ≫ e

theorem

nsmulHom_succ

L380 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nsmulHom_succ

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)

Lean source · full declaration

theorem nsmulHom_succ (k : ℕ) : (nsmulHom c mul hmulK e he (k + 1)).1 =
    pullback.lift (nsmulHom c mul hmulK e he k).1 (𝟙 J)
      (by rw [(nsmulHom c mul hmulK e he k).2, Category.id_comp]) ≫ mul := rfl

theorem

e_comp_nsmulHom

L384 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.e_comp_nsmulHom

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)

Lean source · statement

theorem e_comp_nsmulHom (hee : pullback.lift e e rfl ≫ mul = e) (k : ℕ) :
    e ≫ (nsmulHom c mul hmulK e he k).1 = e

def

transl

L394 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.transl

Documentation

Translation by a rational point using the given multiplication morphism.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)

Lean source · statement

def transl (σ : {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _}) : J ⟶ J

theorem

transl_comp_c

L399 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.transl_comp_c

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section SchemeLevel
variable (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
include hmulK in

Lean source · statement

theorem transl_comp_c (σ) : transl c mul σ ≫ c = c

abbrev

ev

L416 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.ev

Documentation

The residue evaluation of the stalk at the point of the identity section.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)

Lean source · statement

abbrev ev : J.presheaf.stalk (e.base (closedPoint K)) ⟶ CommRingCat.of K

theorem

Φ_ev

L419 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.Φ_ev

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)

Lean source · statement

theorem Φ_ev : Φ (e.base (closedPoint K)) (ev e) = e

theorem

ιO_ev

L423 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.ιO_ev

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
include he in

Lean source · statement

theorem ιO_ev : ιO (e.base (closedPoint K)) c ≫ ev e = 𝟙 _

theorem

ev_ιO_apply

L427 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.ev_ιO_apply

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
include he in

Lean source · statement

theorem ev_ιO_apply (a : K) : (ev e).hom ((ιO (e.base (closedPoint K)) c).hom a) = a

theorem

mem_maximalIdeal_iff_ev

L430 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mem_maximalIdeal_iff_ev

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)

Lean source · statement

theorem mem_maximalIdeal_iff_ev (x : J.presheaf.stalk (e.base (closedPoint K))) :
    x ∈ maximalIdeal _ ↔ (ev e).hom x = 0

theorem

maximalIdeal_eq_ker_ev

L440 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.maximalIdeal_eq_ker_ev

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)

Lean source · statement

theorem maximalIdeal_eq_ker_ev :
    maximalIdeal (J.presheaf.stalk (e.base (closedPoint K))) = RingHom.ker (ev e).hom

theorem

e_idem'

L445 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.e_idem'

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
include hr he in

Lean source · statement

theorem e_idem' : pullback.lift e e rfl ≫ mul = e

theorem

nsmulHom_base

L452 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nsmulHom_base

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
include hr he in

Lean source · statement

theorem nsmulHom_base (n : ℕ) :
    (nsmulHom c mul hmulK e he n).1.base (e.base (closedPoint K)) = e.base (closedPoint K)

theorem

ιO_stalkEndo

L459 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.ιO_stalkEndo

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)

Lean source · statement

theorem ιO_stalkEndo (φ : J ⟶ J) (hφc : φ ≫ c = c) (x₀ : J) (hφ : φ.base x₀ = x₀) :
    ιO x₀ c ≫ stalkEndo x₀ φ hφ = ιO x₀ c

def

IsTestHom

L480 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.IsTestHom

Documentation

A square-zero test map with the prescribed residue evaluation and coefficient inclusion.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

def IsTestHom (g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V) : Prop

theorem

isLocalHom

L483 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.IsTestHom.isLocalHom

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem IsTestHom.isLocalHom {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (hg : IsTestHom c e g) : IsLocalHom g.hom

theorem

isLocalHom_comp'

L493 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.isLocalHom_comp'

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem isLocalHom_comp' {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom f.hom]
    [IsLocalHom g.hom] : IsLocalHom (f ≫ g).hom

theorem

Φcomp

L498 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.IsTestHom.Φcomp

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem IsTestHom.Φcomp {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (hg : IsTestHom c e g) : Φ _ g ≫ c = Spec.map Λinl

theorem

comp_Λmap

L502 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.IsTestHom.comp_Λmap

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem IsTestHom.comp_Λmap {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (hg : IsTestHom c e g) (f : V →ₗ[K] W) : IsTestHom c e (g ≫ Λmap f)

theorem

isTestHom_zero

L509 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.isTestHom_zero

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include he in

Lean source · statement

theorem isTestHom_zero : IsTestHom c e (ev e ≫ (Λinl : _ ⟶ Λ K V))

theorem

Φ_zero

L514 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.Φ_zero

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem Φ_zero : Φ _ (ev e ≫ (Λinl : _ ⟶ Λ K V)) = Spec.map Λinl ≫ e

def

mpt

L518 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mpt

Documentation

The product of the scheme-valued points induced by two compatible square-zero test maps.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

def mpt (g₁ g₂ : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V)
    (h : ιO (e.base (closedPoint K)) c ≫ g₁ = ιO (e.base (closedPoint K)) c ≫ g₂) :
    Spec (Λ K V) ⟶ J

theorem

mpt_congr

L523 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mpt_congr

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem mpt_congr {g₁ g₂ g₁' g₂' : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (h₁ : g₁ = g₁') (h₂ : g₂ = g₂') (h) (h') :
    mpt c mul e g₁ g₂ h = mpt c mul e g₁' g₂' h'

theorem

SpecMap_comp_mpt_lift

L528 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.SpecMap_comp_mpt_lift

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · full declaration

theorem SpecMap_comp_mpt_lift {R : CommRingCat.{u}}
    (g₁ g₂ : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V) (h) (φ : Λ K V ⟶ R) :
    Spec.map φ ≫ mpt c mul e g₁ g₂ h =
      pullback.lift (Φ _ (g₁ ≫ φ)) (Φ _ (g₂ ≫ φ))
        (by rw [Φ_comp_c, Φ_comp_c, reassoc_of% h]) ≫ mul := by
  rw [mpt, comp_pullbackLift_assoc]
  congr 1
  ext : 1 <;> simp only [pullback.lift_fst, pullback.lift_snd, Φ_comp]

theorem

SpecMap_comp_mpt

L537 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.SpecMap_comp_mpt

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · full declaration

theorem SpecMap_comp_mpt
    (g₁ g₂ : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V) (h) (φ : Λ K V ⟶ Λ K W) :
    Spec.map φ ≫ mpt c mul e g₁ g₂ h = mpt c mul e (g₁ ≫ φ) (g₂ ≫ φ) (by rw [reassoc_of% h]) := by
  rw [mpt, mpt, comp_pullbackLift_assoc]
  congr 1
  ext : 1 <;> simp only [pullback.lift_fst, pullback.lift_snd, Φ_comp]

theorem

mpt_zero_right

L545 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mpt_zero_right

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hr in

Lean source · statement

theorem mpt_zero_right {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (hg : IsTestHom c e g) (h) : mpt c mul e g (ev e ≫ Λinl) h = Φ _ g

theorem

mpt_zero_left

L555 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mpt_zero_left

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hl in

Lean source · statement

theorem mpt_zero_left {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K V}
    (hg : IsTestHom c e g) (h) : mpt c mul e (ev e ≫ Λinl) g h = Φ _ g

theorem

exists_test_add

L565 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.exists_test_add

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hmulK hr hl he in

Lean source · full declaration

theorem exists_test_add {g₁ g₂ : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K K}
    (hg₁ : IsTestHom c e g₁) (hg₂ : IsTestHom c e g₂) :
    ∃ g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K K, IsTestHom c e g ∧
      Φ _ g = mpt c mul e g₁ g₂ (by rw [hg₁.2, hg₂.2]) ∧
      ∀ x, (g.hom x).snd = (g₁.hom x).snd + (g₂.hom x).snd := by
  set G₁ := g₁ ≫ Λmap (LinearMap.inl K K K) with hG₁def
  set G₂ := g₂ ≫ Λmap (LinearMap.inr K K K) with hG₂def
  have hG₁ : IsTestHom c e G₁ := IsTestHom.comp_Λmap c e hg₁ _
  have hG₂ : IsTestHom c e G₂ := IsTestHom.comp_Λmap c e hg₂ _
  have hG : ιO _ c ≫ G₁ = ιO _ c ≫ G₂ := by rw [hG₁.2, hG₂.2]
  set M := mpt c mul e G₁ G₂ hG with hMdef
  have hzero : ιO _ c ≫ g₁ = ιO _ c ≫ (ev e ≫ Λinl) := by
    rw [hg₁.2, ← Category.assoc, ιO_ev c e he, Category.id_comp]
  have hzero' : ιO _ c ≫ (ev e ≫ Λinl) = ιO _ c ≫ g₂ := by
    rw [hg₂.2, ← Category.assoc, ιO_ev c e he, Category.id_comp]
  have hM₁ : Spec.map (Λmap (LinearMap.fst K K K)) ≫ M = Φ _ g₁ := by
    have e1 : G₁ ≫ Λmap (LinearMap.fst K K K) = g₁ := by
      rw [hG₁def, Category.assoc, Λmap_comp, LinearMap.fst_comp_inl, Λmap_id, Category.comp_id]
    have e2 : G₂ ≫ Λmap (LinearMap.fst K K K) = ev e ≫ Λinl := by
      rw [hG₂def, Category.assoc, Λmap_comp, LinearMap.fst_comp_inr, Λmap_zero,
        reassoc_of% hg₂.1]
    rw [hMdef, SpecMap_comp_mpt, mpt_congr c mul e e1 e2 _ hzero, mpt_zero_right c mul e he hr hg₁]
  have hM₂ : Spec.map (Λmap (LinearMap.snd K K K)) ≫ M = Φ _ g₂ := by
    have e1 : G₁ ≫ Λmap (LinearMap.snd K K K) = ev e ≫ Λinl := by
      rw [hG₁def, Category.assoc, Λmap_comp, LinearMap.snd_comp_inl, Λmap_zero,
        reassoc_of% hg₁.1]
    have e2 : G₂ ≫ Λmap (LinearMap.snd K K K) = g₂ := by
      rw [hG₂def, Category.assoc, Λmap_comp, LinearMap.snd_comp_inr, Λmap_id, Category.comp_id]
    rw [hMdef, SpecMap_comp_mpt, mpt_congr c mul e e1 e2 _ hzero', mpt_zero_left c mul e he hl hg₂]
  have hMΔ : Spec.map (Λmap (LinearMap.fst K K K + LinearMap.snd K K K)) ≫ M =
      mpt c mul e g₁ g₂ (by rw [hg₁.2, hg₂.2]) := by
    have e1 : G₁ ≫ Λmap (LinearMap.fst K K K + LinearMap.snd K K K) = g₁ := by
      rw [hG₁def, Category.assoc, Λmap_comp, LinearMap.add_comp, LinearMap.fst_comp_inl,
        LinearMap.snd_comp_inl, add_zero, Λmap_id, Category.comp_id]
    have e2 : G₂ ≫ Λmap (LinearMap.fst K K K + LinearMap.snd K K K) = g₂ := by
      rw [hG₂def, Category.assoc, Λmap_comp, LinearMap.add_comp, LinearMap.fst_comp_inr,
        LinearMap.snd_comp_inr, zero_add, Λmap_id, Category.comp_id]
    rw [hMdef, SpecMap_comp_mpt, mpt_congr c mul e e1 e2]
  have hM₀ : Spec.map Λfst ≫ M = e := by
    rw [hMdef, SpecMap_comp_mpt_lift]
    have := e_idem' c mul e he hr
    convert this using 2
    ext : 1 <;> simp only [hG₁.1, Φ_ev, hG₂.1, pullback.lift_fst, pullback.lift_snd]
  have hMx : M.base (closedPoint (TrivSqZeroExt K (K × K))) = e.base (closedPoint K) := by
    have h1 : (Spec.map (Λfst : Λ K (K × K) ⟶ _)).base (closedPoint K) = closedPoint _ :=
      Spec_closedPoint
    rw [← h1]
    conv_rhs => rw [← hM₀]
    rfl
  obtain ⟨gM, hgMloc, hgM⟩ := exists_eq_Φ _ M hMx
  have hev : IsLocalHom (ev e).hom := inferInstance
  have hgM1 : gM ≫ Λfst = ev e := by
    have : IsLocalHom (gM ≫ Λfst).hom := isLocalHom_comp' _ _
    apply Φ_injective
    rw [Φ_comp, hgM, hM₀, Φ_ev]
  have hgM2 : ιO _ c ≫ gM = Λinl := by
    apply Spec.map_injective
    rw [← Φ_comp_c, hgM, hMdef, mpt, Category.assoc, hmulK, pullback.lift_fst_assoc,
      IsTestHom.Φcomp c e hG₁]
  have hgMt : IsTestHom c e gM := ⟨hgM1, hgM2⟩
  have hc1 : gM ≫ Λmap (LinearMap.fst K K K) = g₁ := by
    have := IsTestHom.isLocalHom c e (IsTestHom.comp_Λmap c e hgMt (LinearMap.fst K K K))
    have := IsTestHom.isLocalHom c e hg₁
    apply Φ_injective
    rw [Φ_comp, hgM, hM₁]
  have hc2 : gM ≫ Λmap (LinearMap.snd K K K) = g₂ := by
    have := IsTestHom.isLocalHom c e (IsTestHom.comp_Λmap c e hgMt (LinearMap.snd K K K))
    have := IsTestHom.isLocalHom c e hg₂
    apply Φ_injective
    rw [Φ_comp, hgM, hM₂]
  refine ⟨gM ≫ Λmap (LinearMap.fst K K K + LinearMap.snd K K K),
    IsTestHom.comp_Λmap c e hgMt _, ?_, ?_⟩
  · rw [Φ_comp, hgM, hMΔ]
  · intro x
    rw [← hc1, ← hc2]
    simp only [CommRingCat.hom_comp, ConcreteCategory.hom_ofHom, AlgHom.toRingHom_eq_coe,
      RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, TrivSqZeroExt.snd_map,
      LinearMap.add_apply, LinearMap.fst_apply, LinearMap.snd_apply]

theorem

exists_test_nsmul

L645 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.exists_test_nsmul

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hr hl he in

Lean source · statement

theorem exists_test_nsmul {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K K}
    (hg : IsTestHom c e g) (k : ℕ) :
    ∃ g' : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K K, IsTestHom c e g' ∧
      Φ _ g' = Φ _ g ≫ (nsmulHom c mul hmulK e he k).1 ∧
      ∀ x, (g'.hom x).snd = k • (g.hom x).snd

theorem

test_stalkEndo

L666 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.test_stalkEndo

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hr hl he in

Lean source · statement

theorem test_stalkEndo {g : J.presheaf.stalk (e.base (closedPoint K)) ⟶ Λ K K}
    (hg : IsTestHom c e g) (n : ℕ)
    (hfix : (nsmulHom c mul hmulK e he n).1.base (e.base (closedPoint K)) = e.base (closedPoint K))
    (x : J.presheaf.stalk (e.base (closedPoint K))) :
    (g.hom ((stalkEndo _ _ hfix).hom x)).snd = n • (g.hom x).snd ∧
      (g.hom ((stalkEndo _ _ hfix).hom x)).fst = (ev e).hom x

theorem

stalkEndo_nsmulHom_sub_mem_sq

L688 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.stalkEndo_nsmulHom_sub_mem_sq

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hr hl he in

Lean source · statement

theorem stalkEndo_nsmulHom_sub_mem_sq (n : ℕ)
    (hfix : (nsmulHom c mul hmulK e he n).1.base (e.base (closedPoint K)) =
      e.base (closedPoint K))
    (x : J.presheaf.stalk (e.base (closedPoint K)))
    (hx : x ∈ maximalIdeal (J.presheaf.stalk (e.base (closedPoint K)))) :
    (stalkEndo _ _ hfix).hom x - n • x ∈
      (maximalIdeal (J.presheaf.stalk (e.base (closedPoint K)))) ^ 2

theorem

formallyUnramified_stalkMap_nsmulHom

L717 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.formallyUnramified_stalkMap_nsmulHom

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Tangent
variable {K : Type u} [Field K] {J : Scheme.{u}}
  (c : J ⟶ Spec (.of K)) (mul : pullback c c ⟶ J)
  (hmulK : mul ≫ c = pullback.fst c c ≫ c)
  (e : Spec (.of K) ⟶ J) (he : e ≫ c = 𝟙 _)
  (hr : pullback.lift (𝟙 J) (c ≫ e) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
  (hl : pullback.lift (c ≫ e) (𝟙 J) (by rw [Category.assoc, he, Category.id_comp,
      Category.comp_id]) ≫ mul = 𝟙 J)
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
include hr hl he in

Lean source · statement

theorem formallyUnramified_stalkMap_nsmulHom [LocallyOfFiniteType c]
    (n : ℕ) (_hn : n ≠ 0) (hchar : (n : K) ≠ 0) :
    ((nsmulHom c mul hmulK e he n).1.stalkMap (e.base (closedPoint K))).hom.FormallyUnramified

theorem

isReduced_J

L760 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.isReduced_J

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points

Lean source · statement

theorem isReduced_J (c : J ⟶ Spec (.of K)) [Smooth c] : IsReduced J

theorem

isReduced_pullback

L763 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.isReduced_pullback

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points

Lean source · statement

theorem isReduced_pullback (c : J ⟶ Spec (.of K)) [Smooth c] : IsReduced ↑(pullback c c)

theorem

exists_eq_lift

L773 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.exists_eq_lift

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
omit [IsAlgClosed K] [IsProper c] [Smooth c] [AddCommGroup G] in

Lean source · statement

theorem exists_eq_lift (σ : Spec (.of K) ⟶ pullback c c) (hσ : σ ≫ pullback.fst c c ≫ c = 𝟙 _) :
    ∃ a b : G, σ = pullback.lift (pts a).1 (pts b).1 ((pts a).2.trans (pts b).2.symm)

theorem

mul_comp_c

L783 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.mul_comp_c

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem mul_comp_c : mul ≫ c = pullback.fst c c ≫ c

theorem

rightUnit

L790 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.rightUnit

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · full declaration

theorem rightUnit : pullback.lift (𝟙 J) (c ≫ (pts 0).1) (by rw [Category.assoc, (pts 0).2,
    Category.id_comp, Category.comp_id]) ≫ mul = 𝟙 J := by
  have := isReduced_J c
  have hK := mul_comp_c c mul pts hadd
  refine ext_of_forall_comp_eq_of_isAlgClosed c c ?_ fun σ hσ ↦ ?_
  · rw [Category.assoc, hK, pullback.lift_fst_assoc]
  · obtain ⟨a, rfl⟩ : ∃ a, σ = (pts a).1 :=
      ⟨pts.symm ⟨σ, hσ⟩, (congrArg Subtype.val (pts.apply_symm_apply ⟨σ, hσ⟩)).symm⟩
    rw [comp_pullbackLift_assoc]
    conv_rhs => rw [Category.comp_id, ← add_zero a, hadd]
    congr 1
    ext : 1 <;> simp only [Category.comp_id, reassoc_of% (pts a).2, pullback.lift_fst,
      pullback.lift_snd]

theorem

leftUnit

L804 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.leftUnit

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · full declaration

theorem leftUnit : pullback.lift (c ≫ (pts 0).1) (𝟙 J) (by rw [Category.assoc, (pts 0).2,
    Category.id_comp, Category.comp_id]) ≫ mul = 𝟙 J := by
  have := isReduced_J c
  have hK := mul_comp_c c mul pts hadd
  refine ext_of_forall_comp_eq_of_isAlgClosed c c ?_ fun σ hσ ↦ ?_
  · rw [Category.assoc, hK, pullback.lift_fst_assoc, Category.assoc, (pts 0).2, Category.id_comp,
      Category.comp_id]
  · obtain ⟨a, rfl⟩ : ∃ a, σ = (pts a).1 :=
      ⟨pts.symm ⟨σ, hσ⟩, (congrArg Subtype.val (pts.apply_symm_apply ⟨σ, hσ⟩)).symm⟩
    rw [comp_pullbackLift_assoc]
    conv_rhs => rw [Category.comp_id, ← zero_add a, hadd]
    congr 1
    ext : 1 <;> simp only [reassoc_of% (pts a).2, Category.comp_id, pullback.lift_fst,
      pullback.lift_snd]

theorem

e_idem

L819 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.e_idem

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem e_idem : pullback.lift (pts 0).1 (pts 0).1 rfl ≫ mul = (pts 0).1

theorem

pts_nsmul

L825 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.pts_nsmul

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem pts_nsmul (k : ℕ) (a : G) :
    (pts (k • a)).1 =
      (pts a).1 ≫ (nsmulHom c mul (mul_comp_c c mul pts hadd) (pts 0).1 (pts 0).2 k).1

theorem

pts_comp_transl

L836 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.pts_comp_transl

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd
omit [IsAlgClosed K] [Smooth c] [IsProper c] in

Lean source · statement

theorem pts_comp_transl (a b : G) :
    (pts b).1 ≫ transl c mul (pts a) = (pts (b + a)).1

theorem

transl_comp_transl_neg

L843 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.transl_comp_transl_neg

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem transl_comp_transl_neg (a : G) :
    transl c mul (pts a) ≫ transl c mul (pts (-a)) = 𝟙 J

theorem

isIso_transl

L854 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.isIso_transl

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem isIso_transl (a : G) : IsIso (transl c mul (pts a))

theorem

transl_comp_nsmul

L858 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.transl_comp_nsmul

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Points
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem transl_comp_nsmul (n : ℕ) (a : G) :
    transl c mul (pts a) ≫ (nsmulHom c mul (mul_comp_c c mul pts hadd) (pts 0).1 (pts 0).2 n).1 =
      (nsmulHom c mul (mul_comp_c c mul pts hadd) (pts 0).1 (pts 0).2 n).1 ≫
        transl c mul (pts (n • a))

def

nmul

L884 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nmul

Documentation

The multiplication-by-n morphism supplied by the Picard-group presentation.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

def nmul (n : ℕ) : J ⟶ J

theorem

nmul_comp_c

L888 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nmul_comp_c

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd
omit [ConnectedSpace J] in

Lean source · statement

theorem nmul_comp_c (n : ℕ) : nmul c mul pts hadd n ≫ c = c

theorem

nsmul_base_x₀

L892 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.nsmul_base_x₀

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd
omit [ConnectedSpace J] in

Lean source · statement

theorem nsmul_base_x₀ (n : ℕ) :
    (nmul c mul pts hadd n).base ((pts 0).1.base (closedPoint K)) =
      (pts 0).1.base (closedPoint K)

theorem

exists_etale_nhd_unit

L900 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.exists_etale_nhd_unit

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd
omit [ConnectedSpace J] in

Lean source · statement

theorem exists_etale_nhd_unit (n : ℕ) (hn : n ≠ 0) (hchar : (n : K) ≠ 0) :
    ∃ U : J.Opens, (pts 0).1.base (closedPoint K) ∈ U ∧ Etale (U.ι ≫ nmul c mul pts hadd n)

theorem

etale_nsmul

L910 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.etale_nsmul

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd
omit [ConnectedSpace J] in

Lean source · statement

theorem etale_nsmul (n : ℕ) (hn : n ≠ 0) (hchar : (n : K) ≠ 0) : Etale (nmul c mul pts hadd n)

theorem

exists_nsmul_eq

L959 ↗

JacobianVarieties.Pic0.Proofs.JacobianDivisibility.AlgebraicGeometry.JPHead.exists_nsmul_eq

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace JPHead
variable {K : Type u} [Field K] {J : Scheme.{u}}
section Head
variable [IsAlgClosed K] (c : J ⟶ Spec (.of K)) [Smooth c] [IsProper c]
  [ConnectedSpace J] (mul : pullback c c ⟶ J)
  {G : Type*} [AddCommGroup G] (pts : G ≃ {σ : Spec (.of K) ⟶ J // σ ≫ c = 𝟙 _})
  (hadd : ∀ x y : G, (pts (x + y)).1 =
    pullback.lift (pts x).1 (pts y).1 ((pts x).2.trans (pts y).2.symm) ≫ mul)
include hadd

Lean source · statement

theorem exists_nsmul_eq (n : ℕ) (hn : n ≠ 0) (hchar : (n : K) ≠ 0) (x : G) :
    ∃ y : G, n • y = x

theorem

exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero

L979 ↗

AlgebraicCurve.Pic0.exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.JacobianDivisibility
open _root_.AlgebraicCurve
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.IsLocalRing
universe u

Lean source · statement

theorem _root_.AlgebraicCurve.Pic0.exists_nsmul_eq_of_jacobianPack_of_natCast_ne_zero
    (K F : Type*) [Field K] [Field F] [Algebra K F]
    [IsAlgClosed K]
    (_hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    [IsCurveOver K F]
    (J : AlgebraicGeometry.Scheme)
    (c : J ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
    (hsm : AlgebraicGeometry.Smooth c)
    (hpr : AlgebraicGeometry.IsProper c)
    (hconn : ConnectedSpace J)
    (mul : CategoryTheory.Limits.pullback c c ⟶ J)
    (pts : Pic0 K F ≃
      {σ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ J // σ ≫ c = 𝟙 _})
    (hadd : ∀ x y : Pic0 K F, (pts (x + y)).1 =
      CategoryTheory.Limits.pullback.lift (pts x).1 (pts y).1
        ((pts x).2.trans (pts y).2.symm) ≫ mul)
    (n : ℕ) (hn : n ≠ 0) (hchar : (n : K) ≠ 0) (x : Pic0 K F) :
    ∃ y : Pic0 K F, n • y = x

Module documentation

Divisibility of Picard classes from a Jacobian presentation

Declarations