NYLL
Module

RelativeGroupLaw_isFinite_of_isFinite_endKerStr.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_isFinite_of_isFinite_endKerStr
38 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law is Finite of is Finite end Ker Str

Imports6
Imported by4

Declarations

def

IsHom

L42 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.IsHom
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L50 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.pull_comp
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L57 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.one_coe
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L62 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.pull_one
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L67 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.pull_inv
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L84 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.hom_one
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L93 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.hom_inv
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L109 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.P₀
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₁

L112 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.P₁
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L115 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.t₀
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₁

L118 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.t₁
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L121 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.k₀
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L126 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.x₀
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₁

L130 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.q₁
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₁

L137 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.x₁
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L140 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.k₀_comp
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L148 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.q₁_comp
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

Φ

L155 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Φ
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L164 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Φ_fst
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L167 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Φ_snd
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L171 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.c
Documentation

The difference from the chosen point, giving a morphism into the endomorphism kernel.

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L182 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.c_fst
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L185 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.c_snd
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

Ψ

L189 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ
Documentation

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

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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L192 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_fst
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

L195 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_snd
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L198 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_t₀
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L201 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_pull_k₀
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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₀

L208 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_pull_x₀
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

Ψ_Φ

L214 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Ψ_Φ
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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

Φ_surjective

L227 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.Φ_surjective
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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 Φ_surjective : Function.Surjective (Φ L hβ t ξ)
theorem

preimage_subset_range

L233 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.preimage_subset_range
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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 preimage_subset_range :
    β.1 ⁻¹' Set.range (ξ.1 ≫ β.1) =
      Set.range (Φ L hβ t ξ ≫ pullback.fst β.1 (ξ.1 ≫ β.1))
theorem

finite_P₀

L245 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.finite_P₀
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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β
omit hβ in
Lean source · statement
theorem finite_P₀ [IsFinite (L.endKerStr β)] [Finite T] : Finite (P₀ L t (β := β))
theorem

finite_preimage

L254 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.finite_preimage
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
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 finite_preimage [IsFinite (L.endKerStr β)] [Finite T] :
    (β.1 ⁻¹' Set.range (ξ.1 ≫ β.1)).Finite
theorem

finite_preimage_singleton

L265 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.finite_preimage_singleton
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
include hβ
Lean source · statement
theorem finite_preimage_singleton [IsFinite (L.endKerStr β)] (y : A) :
    (β.1 ⁻¹' {y}).Finite
theorem

locallyQuasiFinite

L292 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.locallyQuasiFinite
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
include hβ
Lean source · statement
theorem locallyQuasiFinite [LocallyOfFiniteType f] [IsFinite (L.endKerStr β)] :
    LocallyQuasiFinite β.1
theorem

isFinite

L299 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_of_isFinite_endKerStr.P2mIsogFin.isFinite
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mIsogFin
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
local infixl:80 " ⊚ " => NeronModelInfra.schemeHomOverComp
variable (L : RelativeGroupLaw K f) {β : SchemeHomOver f f} (hβ : IsHom L β)
include hβ
Lean source · statement
theorem isFinite [IsProper f] [IsFinite (L.endKerStr β)] : IsFinite β.1
theorem

isFinite_of_isFinite_endKerStr

L308 ↗
GoodReductionJacobian.RelativeGroupLaw.isFinite_of_isFinite_endKerStr
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_of_isFinite_endKerStr
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.isFinite_of_isFinite_endKerStr
    (K : Type u) [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K)) [IsProper f]
    (L : RelativeGroupLaw 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 β))
    [IsFinite (L.endKerStr β)] :
    IsFinite β.1

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