NYLL
Module

RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
8 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law locally Quasi Finite scheme Nsmul of finite torsion Subset

Imports9
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  • Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
  • Mathlib.AlgebraicGeometry.ZariskisMainTheorem
  • Mathlib.AlgebraicGeometry.AlgClosed.Basic
  • Mathlib.AlgebraicGeometry.Fiber
  • Mathlib.AlgebraicGeometry.ResidueField
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
  • Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Kernel
Imported by1

Declarations

theorem

finite_of_finite_sections

L38 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.finite_of_finite_sections
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
Lean source · statement
theorem finite_of_finite_sections {K : Type u} [Field K] [IsAlgClosed K] {X : Scheme.{u}}
    (g : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType g]
    (hfin : {σ : Spec (CommRingCat.of K) ⟶ X | σ ≫ g = 𝟙 _}.Finite) : Finite X
theorem

nsmul_coe

L82 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.nsmul_coe
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem nsmul_coe (L : RelativeGroupLaw k f) {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)}
    (m : ℕ) (x : SchemeHomOver t f) : (L.nsmul t m x).1 = x.1 ≫ L.schemeNsmul m
theorem

pow_eq_nsmul

L92 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.pow_eq_nsmul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · full declaration
theorem pow_eq_nsmul (L : RelativeGroupLaw k f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (m : ℕ) (x : SchemeHomOver t f) : (letI := L.pointGroup t; x ^ m) = L.nsmul t m x := by
  let := L.pointGroup t
  induction m with
  | zero => rfl
  | succ m ih => rw [pow_succ, ih, L.nsmul_succ]; rfl
theorem

finite_nsmul_eq

L99 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.finite_nsmul_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem finite_nsmul_eq (L : RelativeGroupLaw k f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t f),
      L.mul t x y = L.mul t y x)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (n : ℕ)
    (hfin : (L.torsionSubset t n).Finite) (y : SchemeHomOver t f) :
    {z : SchemeHomOver t f | L.nsmul t n z = y}.Finite
theorem

finite_sections_pullback

L123 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.finite_sections_pullback
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem finite_sections_pullback (L : RelativeGroupLaw k f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t f),
      L.mul t x y = L.mul t y x)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (n : ℕ)
    (hfin : (L.torsionSubset t n).Finite) (y : SchemeHomOver t f) :
    {σ : T ⟶ pullback (L.schemeNsmul n) y.1 | σ ≫ pullback.snd (L.schemeNsmul n) y.1 = 𝟙 _}.Finite
theorem

quasiFiniteAt_of_isClosed

L152 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.quasiFiniteAt_of_isClosed
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem quasiFiniteAt_of_isClosed [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t f),
      L.mul t x y = L.mul t y x)
    (K : Type u) [Field K] [IsAlgClosed K] [Algebra k K] (n : ℕ)
    (hfin : (L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap k K))) n).Finite)
    [LocallyOfFiniteType (L.schemeNsmul n)]
    (x : G) (hx : IsClosed ({x} : Set G)) : (L.schemeNsmul n).QuasiFiniteAt x
theorem

main

L214 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset.P2mWs11LT.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mWs11LT
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem main [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t f),
      L.mul t x y = L.mul t y x)
    (K : Type u) [Field K] [IsAlgClosed K] [Algebra k K] (n : ℕ)
    (hfin : (L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap k K))) n).Finite) :
    LocallyQuasiFinite (L.schemeNsmul n)
theorem

locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset

L255 ↗
GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
Source context 6 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian in
Lean source · statement
theorem locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset
    {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
    [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t f),
      L.mul t x y = L.mul t y x)
    (K : Type u) [Field K] [IsAlgClosed K] [Algebra k K] (n : ℕ)
    (hfin : (L.torsionSubset (Spec.map (CommRingCat.ofHom (algebraMap k K))) n).Finite) :
    LocallyQuasiFinite (L.schemeNsmul n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.