NYLL
Module

RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
58 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law eq one of sq Zero of nsmul eq one of is Unit

Imports2
Imported by2

Declarations

theorem

schemeHomOverComp_idPoint

L45 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.schemeHomOverComp_idPoint
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem schemeHomOverComp_idPoint {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (x : SchemeHomOver t f) :
    schemeHomOverComp x.1 x.2 (idPoint (f := f)) = x
theorem

nsmul_coe_eq_comp_schemeNsmul

L50 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.nsmul_coe_eq_comp_schemeNsmul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem nsmul_coe_eq_comp_schemeNsmul (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} (n : ℕ) (x : SchemeHomOver t f) :
    (G.nsmul t n x).1 = x.1 ≫ G.schemeNsmul n
theorem

one_coe_eq_comp_one

L59 ↗
GoodReductionJacobian.RelativeGroupLaw.one_coe_eq_comp_one
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.one_coe_eq_comp_one (G :
  RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) :
    (G.one t).1 = t ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

kw_rglnfu_pow_eq_nsmul

L68 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglnfu_pow_eq_nsmul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · full declaration
theorem kw_rglnfu_pow_eq_nsmul (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ) (x : SchemeHomOver t f) :
    (letI := G.pointGroup t; x ^ n) = G.nsmul t n x := by
  let := G.pointGroup t
  induction n with
  | zero => rfl
  | succ n ih => rw [pow_succ, ih, G.nsmul_succ]; rfl
abbrev

KwCommRelGroupLawSqZeroKerNTorsionFree

L78 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.KwCommRelGroupLawSqZeroKerNTorsionFree
Documentation

Every positive multiplication map has trivial kernel on points reducing to the identity across a square-zero ring quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
abbrev KwCommRelGroupLawSqZeroKerNTorsionFree (G : RelativeGroupLaw R f) : Prop
abbrev

KwCommRelGroupLawSqZeroKerNTorsionFreeAt

L87 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.KwCommRelGroupLawSqZeroKerNTorsionFreeAt
Documentation

The fixed multiplication map has trivial kernel on points reducing to the identity across a square-zero ring quotient.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
abbrev KwCommRelGroupLawSqZeroKerNTorsionFreeAt (G : RelativeGroupLaw R f) (n : ℕ) : Prop
theorem

kw_rglcktf_axiomAnchor

L108 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_axiomAnchor
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem kw_rglcktf_axiomAnchor : True
def

kwUnitSection

L114 ↗
GoodReductionJacobian.RelativeGroupLaw.kwUnitSection
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.kwUnitSection (G : RelativeGroupLaw R f)
  : Spec (CommRingCat.of R) ⟶ A
theorem

kwUnitSection_comp

L120 ↗
GoodReductionJacobian.RelativeGroupLaw.kwUnitSection_comp
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.kwUnitSection_comp (G :
  RelativeGroupLaw R f) :
    G.kwUnitSection ≫ f = 𝟙 (Spec (CommRingCat.of R))
theorem

kw_rglcktf_specMap_base_surjective

L127 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_specMap_base_surjective
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem kw_rglcktf_specMap_base_surjective {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
    (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥) :
    Function.Surjective (Spec.map φ).base
theorem

kw_rglcktf_range_subset_of_sqZeroKerElem

L142 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_range_subset_of_sqZeroKerElem
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem kw_rglcktf_range_subset_of_sqZeroKerElem (G : RelativeGroupLaw R f)
    {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
    (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
    (t : Spec R' ⟶ Spec (CommRingCat.of R)) (k : SchemeHomOver t f)
    (hkred : schemeHomOverComp (Spec.map φ) rfl k = G.one (Spec.map φ ≫ t)) :
    Set.range k.1.base ⊆ Set.range G.kwUnitSection.base
def

kwTrivLift

L166 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwTrivLift
Documentation

The algebra map obtained by following the augmentation with the algebra map to the target ring.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
def kwTrivLift : B →ₐ[R] R'
theorem

kw_rglcktf_trivLift_apply

L168 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_trivLift_apply
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
theorem kw_rglcktf_trivLift_apply (x : B) :
    kwTrivLift ε₀ x = algebraMap R R' (ε₀ x)
theorem

kw_rglcktf_mem_kerφ_of_mem_augIdeal

L173 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_mem_kerφ_of_mem_augIdeal
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
theorem kw_rglcktf_mem_kerφ_of_mem_augIdeal (kR : B →ₐ[R] R')
    (hk : ∀ x, φ (kR x) = φ (kwTrivLift ε₀ x))
    {a : B} (ha : a ∈ RingHom.ker ε₀) : kR a ∈ RingHom.ker φ
theorem

kw_rglcktf_eq_zero_of_mem_sq

L181 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_eq_zero_of_mem_sq
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
theorem kw_rglcktf_eq_zero_of_mem_sq (hkerφ : RingHom.ker φ ^ 2 = ⊥)
    (kR : B →ₐ[R] R') (hk : ∀ x, φ (kR x) = φ (kwTrivLift ε₀ x))
    {a : B} (ha : a ∈ (RingHom.ker ε₀) ^ 2) : kR a = 0
theorem

kw_rglcktf_sub_algebraMap_mem_augIdeal

L194 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_sub_algebraMap_mem_augIdeal
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
theorem kw_rglcktf_sub_algebraMap_mem_augIdeal (x : B) :
    x - algebraMap R B (ε₀ x) ∈ RingHom.ker ε₀
theorem

kw_rglcktf_eq_trivLift_of_forall_augIdeal_eq_zero

L199 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_eq_trivLift_of_forall_augIdeal_eq_zero
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
section RingTheory
variable {B R' S' : Type*} [CommRing B] [CommRing R'] [CommRing S']
variable [Algebra R B] [Algebra R R']
variable (ε₀ : B →ₐ[R] R) (φ : R' →+* S')
Lean source · statement
theorem kw_rglcktf_eq_trivLift_of_forall_augIdeal_eq_zero (kR : B →ₐ[R] R')
    (h0 : ∀ a ∈ RingHom.ker ε₀, kR a = 0) : kR = kwTrivLift ε₀
abbrev

kwPairingMap

L214 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwPairingMap
Documentation

The structure morphism of the self fiber product used to evaluate the relative group multiplication.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
Lean source · statement
abbrev kwPairingMap : Limits.pullback f f ⟶ Spec (CommRingCat.of R)
abbrev

kwPrFst

L218 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwPrFst
Documentation

The first fiber-product projection viewed as a point over its structure morphism.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
Lean source · statement
abbrev kwPrFst : SchemeHomOver (kwPairingMap (f := f)) f
abbrev

kwPrSnd

L222 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwPrSnd
Documentation

The second fiber-product projection viewed as a point over its structure morphism.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
Lean source · statement
abbrev kwPrSnd : SchemeHomOver (kwPairingMap (f := f)) f
def

kwSchemeMul

L225 ↗
GoodReductionJacobian.RelativeGroupLaw.kwSchemeMul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
Lean source · statement
def _root_.GoodReductionJacobian.RelativeGroupLaw.kwSchemeMul (G : RelativeGroupLaw R f) :
  Limits.pullback f f ⟶ A
theorem

kwSchemeMul_over

L231 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwSchemeMul_over
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem kwSchemeMul_over (G : RelativeGroupLaw R f) :
    G.kwSchemeMul ≫ f = kwPairingMap (f := f)
theorem

kw_rglcktf_mul_coe_eq_lift_comp_schemeMul

L235 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_mul_coe_eq_lift_comp_schemeMul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem kw_rglcktf_mul_coe_eq_lift_comp_schemeMul (G : RelativeGroupLaw R f)
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x y : SchemeHomOver t f) :
    (G.mul t x y).1 = Limits.pullback.lift x.1 y.1 (x.2.trans y.2.symm) ≫ G.kwSchemeMul
theorem

kw_rglcktf_schemeMul_unitPair

L253 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktf_schemeMul_unitPair
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory.Limits
open _root_.GoodReductionJacobian.RelativeGroupLaw
Lean source · statement
theorem kw_rglcktf_schemeMul_unitPair (G : RelativeGroupLaw R f) :
    Limits.pullback.lift G.kwUnitSection G.kwUnitSection rfl ≫ G.kwSchemeMul
      = G.kwUnitSection
theorem

kw_rglcktfm_axiomAnchor

L276 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_axiomAnchor
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem kw_rglcktfm_axiomAnchor : True
abbrev

kwTensorPair

L287 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwTensorPair
Documentation

The algebra map on the tensor product extending the two given algebra maps.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section FourTerm
variable {B C : Type*} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C]
Lean source · statement
abbrev kwTensorPair (p q : B →ₐ[R] C) : (B ⊗[R] B) →ₐ[R] C
theorem

kw_rglcktfm_fourTerm_tensorPair

L290 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_fourTerm_tensorPair
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section FourTerm
variable {B C : Type*} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C]
Lean source · statement
theorem kw_rglcktfm_fourTerm_tensorPair (ε₀ : B →ₐ[R] R) {J : Ideal C} (hJ2 : J ^ 2 = ⊥)
    (p q : B →ₐ[R] C) (hp : ∀ a ∈ RingHom.ker ε₀, p a ∈ J)
    (hq : ∀ a ∈ RingHom.ker ε₀, q a ∈ J) (z : B ⊗[R] B) :
    kwTensorPair p q z - kwTensorPair p (kwTrivLift ε₀) z
      - kwTensorPair (kwTrivLift ε₀) q z
      + kwTensorPair (kwTrivLift ε₀) (kwTrivLift ε₀) z = 0
theorem

kw_rglcktfm_tensorPair_lifts_trivLift

L313 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_tensorPair_lifts_trivLift
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section FourTerm
variable {B C : Type*} [CommRing B] [CommRing C] [Algebra R B] [Algebra R C]
Lean source · statement
theorem kw_rglcktfm_tensorPair_lifts_trivLift (ε₀ : B →ₐ[R] R) {S' : Type*} [CommRing S']
    (φ : C →+* S') (p q : B →ₐ[R] C)
    (hp : ∀ b, φ (p b) = φ (kwTrivLift ε₀ b)) (hq : ∀ b, φ (q b) = φ (kwTrivLift ε₀ b))
    (z : B ⊗[R] B) :
    φ (kwTensorPair p q z)
      = φ (kwTrivLift (kwTensorPair ε₀ ε₀) z)
def

KwIsKerElt

L338 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.KwIsKerElt
Documentation

A relative point belongs to the reduction kernel when its reduction is the identity point.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
def KwIsKerElt (k : SchemeHomOver t f) : Prop
theorem

kw_rglcktfm_isKerElt_one

L341 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_isKerElt_one
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_isKerElt_one : KwIsKerElt G φ t (G.one t)
theorem

kw_rglcktfm_isKerElt_mul

L344 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_isKerElt_mul
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_isKerElt_mul {x y : SchemeHomOver t f}
    (hx : KwIsKerElt G φ t x) (hy : KwIsKerElt G φ t y) :
    KwIsKerElt G φ t (G.mul t x y)
theorem

kw_rglcktfm_isKerElt_nsmul

L350 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_isKerElt_nsmul
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_isKerElt_nsmul {k : SchemeHomOver t f} (hk : KwIsKerElt G φ t k)
    (m : ℕ) : KwIsKerElt G φ t (G.nsmul t m k)
def

kwKerRing

L357 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwKerRing
Documentation

The ring map representing a reduction-kernel point in the chosen affine open chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
def kwKerRing (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k) : B₁ ⟶ R'
theorem

kw_rglcktfm_map_kerRing

L361 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_map_kerRing
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_map_kerRing (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k) :
    Spec.map (kwKerRing G B₁ ι hιe φ hsurj hker t k hk) ≫ ι = k.1
theorem

kw_rglcktfm_eq_of_kerRing_eq

L365 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_eq_of_kerRing_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_eq_of_kerRing_eq {k k' : SchemeHomOver t f}
    (hk : KwIsKerElt G φ t k) (hk' : KwIsKerElt G φ t k')
    (h : kwKerRing G B₁ ι hιe φ hsurj hker t k hk
      = kwKerRing G B₁ ι hιe φ hsurj hker t k' hk') : k = k'
theorem

kw_rglcktfm_kerRing_reduces

L373 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerRing_reduces
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section AffineBridge
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem kw_rglcktfm_kerRing_reduces (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k) :
    ∀ b, φ.hom ((kwKerRing G B₁ ι hιe φ hsurj hker t k hk).hom b)
      = φ.hom ((kwKerRing G B₁ ι hιe φ hsurj hker t (G.one t)
          (kw_rglcktfm_isKerElt_one G φ t)).hom b)
theorem

kw_rglcktfm_preimage_lift_algebraMap

L404 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_preimage_lift_algebraMap
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_preimage_lift_algebraMap {T : CommRingCat.{u}}
    (g : Spec T ⟶ A) (hrange : Set.range g.base ⊆ Set.range ι.base)
    (algT : CommRingCat.of R ⟶ T) (hg : g ≫ f = Spec.map algT) (r : R) :
    (Spec.preimage (IsOpenImmersion.lift ι g hrange)).hom (algebraMap R B₁ r)
      = algT.hom r
def

kwAug

L418 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwAug
Documentation

The augmentation of the affine chart obtained by evaluating at the relative identity section.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
def kwAug : (B₁ : Type u) →ₐ[R] R
theorem

kw_rglcktfm_map_aug

L424 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_map_aug
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_map_aug :
    Spec.map (CommRingCat.ofHom (kwAug G B₁ ι hιf hιe).toRingHom) ≫ ι
      = G.kwUnitSection
def

kwTensorStruct

L434 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwTensorStruct
Documentation

The structure morphism of the spectrum of the tensor product of the affine chart rings.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
omit hιf in
Lean source · statement
def kwTensorStruct : Spec (CommRingCat.of ((B₁ : Type u) ⊗[R] B₁))
    ⟶ Spec (CommRingCat.of R)
def

kwTensorPoint

L439 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwTensorPoint
Documentation

An algebra map from the chart ring defines a relative point over the tensor-product spectrum.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
def kwTensorPoint (ρ : (B₁ : Type u) →ₐ[R] ((B₁ : Type u) ⊗[R] B₁)) :
    SchemeHomOver (kwTensorStruct (R := R) B₁) f
def

kwUniversalMul

L448 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwUniversalMul
Documentation

The product of the two universal affine-chart points over the tensor-product spectrum.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
def kwUniversalMul : Spec (CommRingCat.of ((B₁ : Type u) ⊗[R] B₁)) ⟶ A
abbrev

kwAugAug

L453 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwAugAug
Documentation

The tensor-product augmentation extending the affine-chart augmentation in both factors.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
abbrev kwAugAug : ((B₁ : Type u) ⊗[R] B₁) →ₐ[R] R
theorem

kw_rglcktfm_augAug_surjective

L456 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_augAug_surjective
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_augAug_surjective :
    Function.Surjective (kwAugAug G B₁ ι hιf hιe)
theorem

kw_rglcktfm_universalMul_aug

L460 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_universalMul_aug
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_universalMul_aug :
    Spec.map (CommRingCat.ofHom (kwAugAug G B₁ ι hιf hιe).toRingHom)
      ≫ kwUniversalMul G B₁ ι hιf = G.kwUnitSection
theorem

kw_rglcktfm_range_truncMul_subset

L486 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_range_truncMul_subset
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_range_truncMul_subset :
    Set.range (Spec.map (CommRingCat.ofHom
        (Ideal.Quotient.mk (RingHom.ker (kwAugAug G B₁ ι hιf hιe).toRingHom ^ 2)))
      ≫ kwUniversalMul G B₁ ι hιf).base ⊆ Set.range ι.base
def

kwMBar

L515 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwMBar
Documentation

The chart ring map for universal multiplication after quotienting by the square of the tensor-product augmentation ideal.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
def kwMBar : B₁ ⟶ CommRingCat.of
    (((B₁ : Type u) ⊗[R] B₁) ⧸ RingHom.ker (kwAugAug G B₁ ι hιf hιe).toRingHom ^ 2)
theorem

kw_rglcktfm_map_mBar

L519 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_map_mBar
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
Lean source · statement
theorem kw_rglcktfm_map_mBar :
    Spec.map (kwMBar G B₁ ι hιf hιe) ≫ ι
      = Spec.map (CommRingCat.ofHom
          (Ideal.Quotient.mk (RingHom.ker (kwAugAug G B₁ ι hιf hιe).toRingHom ^ 2)))
        ≫ kwUniversalMul G B₁ ι hιf
def

kwKerAlg

L535 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kwKerAlg
Documentation

The chart ring map of a reduction-kernel point, viewed as an algebra map using the base compatibility equation.

Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include hιe htR' in
Lean source · statement
def kwKerAlg (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k) :
    (B₁ : Type u) →ₐ[R] R'
theorem

kw_rglcktfm_kerAlg_apply

L542 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_apply
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_apply (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k)
    (b : B₁) :
    kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' k hk b
      = (kwKerRing G B₁ ι hιe φ hsurj hker t k hk).hom b
theorem

kw_rglcktfm_kerAlg_one

L548 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_one
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_one :
    kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.one t) (kw_rglcktfm_isKerElt_one G φ t)
      = kwTrivLift (kwAug G B₁ ι hιf hιe)
theorem

kw_rglcktfm_mul_eq_tensorPair_universalMul

L565 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_mul_eq_tensorPair_universalMul
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_mul_eq_tensorPair_universalMul
    (x y : SchemeHomOver t f) (hx : KwIsKerElt G φ t x) (hy : KwIsKerElt G φ t y) :
    (G.mul t x y).1
      = Spec.map (CommRingCat.ofHom (kwTensorPair
          (kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' x hx)
          (kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' y hy)).toRingHom)
        ≫ kwUniversalMul G B₁ ι hιf
theorem

kw_rglcktfm_kerAlg_val_eq

L598 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_val_eq
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_val_eq {k k' : SchemeHomOver t f}
    (hk : KwIsKerElt G φ t k) (hk' : KwIsKerElt G φ t k') (h : k = k') (b : B₁) :
    kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' k hk b
      = kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' k' hk' b
theorem

kw_rglcktfm_kerAlg_reduces

L604 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_reduces
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_reduces (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k)
    (b : B₁) :
    φ.hom (kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' k hk b)
      = φ.hom (kwTrivLift (kwAug G B₁ ι hιf hιe) b)
theorem

kw_rglcktfm_kerAlg_mul_fourTerm

L612 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_mul_fourTerm
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_mul_fourTerm (x y : SchemeHomOver t f)
    (hx : KwIsKerElt G φ t x) (hy : KwIsKerElt G φ t y) (b : B₁) :
    kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.mul t x y)
        (kw_rglcktfm_isKerElt_mul G φ t hx hy) b
      - kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' x hx b
      - kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' y hy b
      + kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.one t)
          (kw_rglcktfm_isKerElt_one G φ t) b = 0
theorem

kw_rglcktfm_kerAlg_nsmul_sub

L676 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglcktfm_kerAlg_nsmul_sub
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
section TensorArgument
open Algebra.TensorProduct
variable (G : RelativeGroupLaw R f)
variable (B₁ : CommRingCat.{u}) [Algebra R B₁]
variable (ι : Spec B₁ ⟶ A) [IsOpenImmersion ι]
variable (hιf : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R B₁)))
variable (hιe : Set.range G.kwUnitSection.base ⊆ Set.range ι.base)
include hιf
variable {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
variable (hsurj : Function.Surjective φ) (hker : RingHom.ker φ.hom ^ 2 = ⊥)
variable (t : Spec R' ⟶ Spec (CommRingCat.of R))
variable [Algebra R R'] (htR' : (algebraMap R R' : R →+* R') = (Spec.preimage t).hom)
include htR' in
Lean source · statement
theorem kw_rglcktfm_kerAlg_nsmul_sub (k : SchemeHomOver t f) (hk : KwIsKerElt G φ t k)
    (m : ℕ) (b : B₁) :
    kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.nsmul t m k)
        (kw_rglcktfm_isKerElt_nsmul G φ t hk m) b
      - kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.one t)
          (kw_rglcktfm_isKerElt_one G φ t) b
    = m • (kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' k hk b
      - kwKerAlg G B₁ ι hιf hιe φ hsurj hker t htR' (G.one t)
          (kw_rglcktfm_isKerElt_one G φ t) b)
theorem

kw_rglckf_sqZeroKerNTorsionFreeAt_of_isUnit

L723 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit.GoodReductionJacobian.RelativeGroupLaw.kw_rglckf_sqZeroKerNTorsionFreeAt_of_isUnit
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
noncomputable section
section IsUnitDischarge
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits NeronModelInfra
namespace GoodReductionJacobian
open _root_.GoodReductionJacobian
open _root_.GoodReductionJacobian
namespace RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [Field R]
variable {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem kw_rglckf_sqZeroKerNTorsionFreeAt_of_isUnit (G : RelativeGroupLaw R f)
    {n : ℕ} (hn : IsUnit (n : R)) :
    KwCommRelGroupLawSqZeroKerNTorsionFreeAt G n
theorem

eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit

L774 ↗
GoodReductionJacobian.RelativeGroupLaw.eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped TensorProduct
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra _root_.GoodReductionJacobian
  GoodReductionJacobian in
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit
    {R : Type u} [Field R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) (n : ℕ) (hn : IsUnit (n : R))
    (R' S' : CommRingCat.{u}) (φ : R' ⟶ S') (hφ : Function.Surjective φ)
    (hker : RingHom.ker φ.hom ^ 2 = ⊥)
    (t : Spec R' ⟶ Spec (CommRingCat.of R)) (k : SchemeHomOver t f)
    (hk : schemeHomOverComp (Spec.map φ) rfl k = G.one (Spec.map φ ≫ t))
    (hnk : G.nsmul t n k = G.one t) :
    k = G.one t

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