NYLL
Module

RelativeGroupLaw_isFinite_endKerStr_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_isFinite_endKerStr_of_surjective
52 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law is Finite end Ker Str of surjective

Imports18
Imported by2

Declarations

theorem

isIntegral_quotient_of_generators

L53 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.isIntegral_quotient_of_generators
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Alg
open _root_.Polynomial
Lean source · statement
theorem isIntegral_quotient_of_generators {R C : Type*} [CommRing R] [CommRing C] [Algebra R C]
    (s : Finset C) (hs : Algebra.adjoin R (s : Set C) = ⊤) (r : R)
    (hint : ∀ z ∈ s, IsIntegral R (r • z)) (m : Ideal R) [m.IsMaximal] (hrm : r ∉ m) :
    Algebra.IsIntegral (R ⧸ m) (C ⧸ m.map (algebraMap R C))
theorem

exists_ne_zero_forall_finite_liesOver

L86 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.exists_ne_zero_forall_finite_liesOver
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Alg
open _root_.Polynomial
Lean source · statement
theorem exists_ne_zero_forall_finite_liesOver (R C : Type*) [CommRing R] [IsDomain R] [CommRing C]
    [Algebra R C] [Algebra.FiniteType R C] [Algebra.IsAlgebraic R C] :
    ∃ r : R, r ≠ 0 ∧ ∀ (m : Ideal R), m.IsMaximal → r ∉ m →
      {Q : PrimeSpectrum C | Q.asIdeal.comap (algebraMap R C) = m}.Finite
theorem

isAlgebraic_of_trdeg_eq

L122 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.isAlgebraic_of_trdeg_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Alg
open _root_.Polynomial
universe u₁ u₂ u₃
Lean source · statement
theorem isAlgebraic_of_trdeg_eq (K : Type u₁) (R : Type u₂) (C : Type u₃) [Field K] [CommRing R]
    [IsDomain R] [CommRing C] [IsDomain C] [Algebra K R] [Algebra K C] [Algebra R C]
    [IsScalarTower K R C] [Algebra.FiniteType K R] (hinj : Function.Injective (algebraMap R C))
    (h : Cardinal.lift.{u₃} (Algebra.trdeg K R) = Cardinal.lift.{u₂} (Algebra.trdeg K C)) :
    Algebra.IsAlgebraic R C
def

algK

L157 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.algK
Documentation

The coefficient-field homomorphism to sections on an open of the group scheme.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
def algK (U : A.Opens) : K →+* Γ(A, U)
theorem

map_comp_algK

L160 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.map_comp_algK
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem map_comp_algK {U V : A.Opens} (i : V ≤ U) :
    (A.presheaf.map (homOfLE i).op).hom.comp (algK f U) = algK f V
def

algFF

L171 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.algFF
Documentation

The coefficient-field homomorphism to the function field, defined through the generic-point germ.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
def algFF [IrreducibleSpace A] : K →+* A.functionField
theorem

germ_comp_algK

L175 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.germ_comp_algK
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem germ_comp_algK [IrreducibleSpace A] (U : A.Opens) [hU : Nonempty U] :
    (A.germToFunctionField U).hom.comp (algK f U) = algFF f
theorem

trdeg_sections_eq

L185 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.trdeg_sections_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · full declaration
theorem trdeg_sections_eq [IsIntegral A] (U : A.Opens) (hU : IsAffineOpen U) [Nonempty U] :
    let _ := (algK f U).toAlgebra
    let _ := (algFF f).toAlgebra
    Algebra.trdeg K Γ(A, U) = Algebra.trdeg K A.functionField := by
  let _ := (algK f U).toAlgebra
  let _ := (algFF f).toAlgebra
  let _ : IsScalarTower K Γ(A, U) A.functionField :=
    IsScalarTower.of_algebraMap_eq' (germ_comp_algK f U).symm
  let _ := functionField_isFractionRing_of_isAffineOpen A U hU
  let _ : FaithfulSMul K Γ(A, U) :=
    (faithfulSMul_iff_algebraMap_injective K _).mpr (algebraMap K Γ(A, U)).injective
  let _ : FaithfulSMul Γ(A, U) A.functionField :=
    (faithfulSMul_iff_algebraMap_injective _ _).mpr (IsFractionRing.injective Γ(A, U) _)
  have halg : Algebra.IsAlgebraic Γ(A, U) A.functionField :=
    IsLocalization.isAlgebraic _ (nonZeroDivisors Γ(A, U))
  have h0 : Algebra.trdeg Γ(A, U) (A.functionField : Type u) = 0 := trdeg_eq_zero_iff.mpr halg
  have hadd := trdeg_add_eq K Γ(A, U) (A := (A.functionField : Type u))
  rw [h0, add_zero] at hadd
  exact hadd
theorem

appLE_congr_hom

L205 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.appLE_congr_hom
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
omit [Field K] in
Lean source · statement
theorem appLE_congr_hom {X Y : Scheme.{u}} {g g' : X ⟶ Y} (h : g = g') (U : Y.Opens) (V : X.Opens)
    (e : V ≤ g ⁻¹ᵁ U) (e' : V ≤ g' ⁻¹ᵁ U) : g.appLE U V e = g'.appLE U V e'
theorem

appLE_comp_algK

L212 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.appLE_comp_algK
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
variable (γ : A ⟶ A) (hγ : γ ≫ f = f)
include hγ
Lean source · statement
theorem appLE_comp_algK {U W : A.Opens} (e : W ≤ γ ⁻¹ᵁ U) :
    (γ.appLE U W e).hom.comp (algK f U) = algK f W
theorem

appLE_injective

L221 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.appLE_injective
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
variable (γ : A ⟶ A) (hγ : γ ≫ f = f)
include hγ
omit hγ in
Lean source · statement
theorem appLE_injective [IsIntegral A] (hsurj : Function.Surjective γ) {U W : A.Opens} [hW :
  Nonempty W]
    (e : W ≤ γ ⁻¹ᵁ U) : Function.Injective (γ.appLE U W e).hom
theorem

exists_forall_finite_fibre_inter

L243 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.exists_forall_finite_fibre_inter
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Sections
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
variable (γ : A ⟶ A) (hγ : γ ≫ f = f)
include hγ
Lean source · statement
theorem exists_forall_finite_fibre_inter [IsIntegral A] [LocallyOfFiniteType f] (hsurj :
  Function.Surjective γ)
    {U W : A.Opens} (hU : IsAffineOpen U) (hW : IsAffineOpen W) [Nonempty U] [Nonempty W]
    (e : W ≤ γ ⁻¹ᵁ U) :
    ∃ r : Γ(A, U), r ≠ 0 ∧ ∀ (y : A) (_ : y ∈ U), IsClosed ({y} : Set A) → y ∈ A.basicOpen r →
      {p : A | p ∈ W ∧ γ p = y}.Finite
theorem

finiteType_algK

L317 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.finiteType_algK
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section KPoints
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem finiteType_algK [LocallyOfFiniteType f] {W : A.Opens} (hW : IsAffineOpen W) :
    (algK f W).FiniteType
theorem

exists_section_mem

L325 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.exists_section_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section KPoints
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem exists_section_mem [IsAlgClosed K] [LocallyOfFiniteType f] (V : A.Opens)
    (hV : (V : Set A).Nonempty) :
    ∃ a : Spec (CommRingCat.of K) ⟶ A, a ≫ f = 𝟙 _ ∧ ∀ s, a s ∈ V
def

IsHom

L375 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.IsHom
Documentation

Compatibility of an endomorphism over the base with the relative group multiplication.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
Lean source · statement
def IsHom (L : RelativeGroupLaw K f) (β : SchemeHomOver f f) : Prop
theorem

pull_comp

L383 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.pull_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
Lean source · statement
theorem pull_comp {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of K)}
    {t' : T' ⟶ Spec (CommRingCat.of K)} (ψ : T' ⟶ T) (hψ : ψ ≫ t = t')
    (x : SchemeHomOver t f) (β : SchemeHomOver f f) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (x ⊚ β) =
      (GoodReductionJacobian.schemeHomOverComp ψ hψ x) ⊚ β
theorem

one_coe

L390 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.one_coe
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
Lean source · statement
theorem one_coe {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) :
    (L.one t).1 = t ≫ (L.one (𝟙 (Spec (CommRingCat.of K)))).1
theorem

pull_one

L395 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.pull_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
Lean source · statement
theorem pull_one {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of K)}
    {t' : T' ⟶ Spec (CommRingCat.of K)} (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (L.one t) = L.one t'
theorem

pull_inv

L400 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.pull_inv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
Lean source · statement
theorem pull_inv {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of K)}
    {t' : T' ⟶ Spec (CommRingCat.of K)} (ψ : T' ⟶ T) (hψ : ψ ≫ t = t')
    (x : SchemeHomOver t f) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (L.inv t x) =
      L.inv t' (GoodReductionJacobian.schemeHomOverComp ψ hψ x)
theorem

hom_one

L417 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.hom_one
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
variable {L}
variable {β : SchemeHomOver f f} (hβ : IsHom L β)
include hβ
Lean source · statement
theorem hom_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) :
    (L.one t) ⊚ β = L.one t
theorem

hom_inv

L426 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.hom_inv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Points
variable (L : RelativeGroupLaw K f)
variable {L}
variable {β : SchemeHomOver f f} (hβ : IsHom L β)
include hβ
Lean source · statement
theorem hom_inv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (x : SchemeHomOver t f) :
    (L.inv t x) ⊚ β = L.inv t (x ⊚ β)
abbrev

P₀

L442 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.P₀
Documentation

The base change of the endomorphism kernel along the chosen test scheme.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
abbrev P₀ : Scheme.{u}
abbrev

P₁

L445 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.P₁
Documentation

The pullback of the endomorphism along the image of the chosen point.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
abbrev P₁ : Scheme.{u}
abbrev

t₀

L448 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.t₀
Documentation

The structure morphism of the kernel base change to the base field spectrum.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
abbrev t₀ : P₀ L t (β := β) ⟶ Spec (CommRingCat.of K)
abbrev

t₁

L451 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.t₁
Documentation

The structure morphism of the endomorphism fibre pullback to the base field spectrum.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
abbrev t₁ : P₁ t ξ (β := β) ⟶ Spec (CommRingCat.of K)
def

k₀

L454 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.k₀
Documentation

The kernel point on its base change, viewed as a point of the group scheme.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
def k₀ : SchemeHomOver (t₀ L t (β := β)) f
def

x₀

L459 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.x₀
Documentation

The chosen test point pulled back to the kernel base change.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
def x₀ : SchemeHomOver (t₀ L t (β := β)) f
def

q₁

L463 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.q₁
Documentation

The group scheme point given by the first projection of the endomorphism fibre pullback.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
def q₁ : SchemeHomOver (t₁ t ξ (β := β)) f
def

x₁

L470 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.x₁
Documentation

The chosen test point pulled back to the endomorphism fibre pullback.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
def x₁ : SchemeHomOver (t₁ t ξ (β := β)) f
theorem

k₀_comp

L473 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.k₀_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
theorem k₀_comp : (k₀ L t (β := β)) ⊚ β = L.one (t₀ L t (β := β))
theorem

q₁_comp

L481 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.q₁_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
Lean source · statement
theorem q₁_comp : (q₁ t ξ (β := β)) ⊚ β = (x₁ t ξ (β := β)) ⊚ β
def

Φ

L488 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ
Documentation

Translation by the chosen point from the kernel base change to the endomorphism fibre.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
def Φ : P₀ L t (β := β) ⟶ P₁ t ξ (β := β)
theorem

Φ_fst

L497 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_fst
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_fst : Φ L hβ t ξ ≫ pullback.fst β.1 (ξ.1 ≫ β.1) = (L.mul _ (k₀ L t) (x₀ L t ξ)).1
theorem

Φ_snd

L500 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_snd : Φ L hβ t ξ ≫ pullback.snd β.1 (ξ.1 ≫ β.1) = pullback.snd (L.endKerStr β) t
def

c

L504 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.c
Documentation

The morphism to the kernel obtained by taking the quotient of two points with the same image.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
def c : P₁ t ξ (β := β) ⟶ L.endKer β
theorem

c_fst

L515 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.c_fst
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem c_fst : c L hβ t ξ ≫ L.endKerι β = (L.mul _ (q₁ t ξ) (L.inv _ (x₁ t ξ))).1
theorem

c_snd

L518 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.c_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem c_snd : c L hβ t ξ ≫ L.endKerStr β = t₁ t ξ (β := β)
def

Ψ

L522 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ
Documentation

The inverse translation from the endomorphism fibre to the kernel base change.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
def Ψ : P₁ t ξ (β := β) ⟶ P₀ L t (β := β)
theorem

Ψ_fst

L525 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_fst
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_fst : Ψ L hβ t ξ ≫ pullback.fst (L.endKerStr β) t = c L hβ t ξ
theorem

Ψ_snd

L528 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_snd
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_snd : Ψ L hβ t ξ ≫ pullback.snd (L.endKerStr β) t = pullback.snd β.1 (ξ.1 ≫ β.1)
theorem

Ψ_t₀

L531 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_t₀
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_t₀ : Ψ L hβ t ξ ≫ t₀ L t (β := β) = t₁ t ξ (β := β)
theorem

Ψ_pull_k₀

L534 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_pull_k₀
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_pull_k₀ :
    GoodReductionJacobian.schemeHomOverComp (Ψ L hβ t ξ) (Ψ_t₀ L hβ t ξ) (k₀ L t) =
      L.mul _ (q₁ t ξ) (L.inv _ (x₁ t ξ))
theorem

Ψ_pull_x₀

L541 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_pull_x₀
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_pull_x₀ :
    GoodReductionJacobian.schemeHomOverComp (Ψ L hβ t ξ) (Ψ_t₀ L hβ t ξ) (x₀ L t ξ) = x₁ t ξ
theorem

Ψ_Φ

L547 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Ψ_Φ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Ψ_Φ : Ψ L hβ t ξ ≫ Φ L hβ t ξ = 𝟙 _
theorem

Φ_t₁

L560 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_t₁
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_t₁ : Φ L hβ t ξ ≫ t₁ t ξ (β := β) = t₀ L t (β := β)
theorem

Φ_pull_q₁

L563 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_pull_q₁
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_pull_q₁ :
    GoodReductionJacobian.schemeHomOverComp (Φ L hβ t ξ) (Φ_t₁ L hβ t ξ) (q₁ t ξ) =
      L.mul _ (k₀ L t) (x₀ L t ξ)
theorem

Φ_pull_x₁

L570 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_pull_x₁
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_pull_x₁ :
    GoodReductionJacobian.schemeHomOverComp (Φ L hβ t ξ) (Φ_t₁ L hβ t ξ) (x₁ t ξ) = x₀ L t ξ
theorem

Φ_Ψ

L576 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_Ψ
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_Ψ : Φ L hβ t ξ ≫ Ψ L hβ t ξ = 𝟙 _
theorem

Φ_injective

L592 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.Φ_injective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section GroupLaw
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
section Translate
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (ξ : SchemeHomOver t f)
include hβ
Lean source · statement
theorem Φ_injective : Function.Injective (Φ L hβ t ξ)
theorem

exists_open_forall_finite_fibre

L609 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.exists_open_forall_finite_fibre
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Main
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] [IsAlgClosed K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
omit [IsAlgClosed K] in
Lean source · statement
theorem exists_open_forall_finite_fibre [IsIntegral A] [IsProper f] (γ : A ⟶ A) (hγ : γ ≫ f = f)
    (hsurj : Function.Surjective γ) :
    ∃ V : A.Opens, (V : Set A).Nonempty ∧ ∀ y ∈ V, IsClosed ({y} : Set A) → (γ ⁻¹' {y}).Finite
theorem

isFinite_endKerStr

L674 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_of_surjective.P2mSurjIsog.isFinite_endKerStr
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
namespace P2mSurjIsog
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
section Main
open NeronModelInfra GoodReductionJacobian
variable {K : Type u} [Field K] [IsAlgClosed K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem isFinite_endKerStr (L : RelativeGroupLaw K f) (hA : AbelianSchemePropertyBundle K f)
    {γ : SchemeHomOver f f} (hγ : IsHom L γ) (hsurj : Function.Surjective γ.1) :
    IsFinite (L.endKerStr γ)
theorem

isFinite_endKerStr_of_surjective

L742 ↗
GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_of_surjective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_of_surjective
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian in
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_of_surjective
    (K : Type u) [Field K] [IsAlgClosed K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
    (L : RelativeGroupLaw K f) (hA : AbelianSchemePropertyBundle K f)
    (γ : SchemeHomOver f f)
    (hγ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (x y : SchemeHomOver t f),
      NeronModelInfra.schemeHomOverComp (L.mul t x y) γ =
        L.mul t (NeronModelInfra.schemeHomOverComp x γ) (NeronModelInfra.schemeHomOverComp y γ))
    [Surjective γ.1] :
    IsFinite (L.endKerStr γ)

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