NYLL
Module

RelativeGroupLaw_exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex
92 declarations indexed from sourceView source ↗

Module documentation

The identity component of a smooth relative group

The identity component is an irreducible open subgroup of finite index.

Imports7
Imported by3

Declarations

def

const

L49 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const
Documentation

The constant point over a scheme determined by a rational point.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def const {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (s : SchemeHomOver pt gN) :
    SchemeHomOver t gN
theorem

const_coe

L53 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const_coe
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem const_coe {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (s : SchemeHomOver pt gN) :
    (const t s).1 = t ≫ s.1
theorem

const_pt

L56 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const_pt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem const_pt (s : SchemeHomOver pt gN) : const pt s = s
theorem

const_transition

L59 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const_transition
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem const_transition {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (t' : T' ⟶ Spec (CommRingCat.of k)) (ψ : T' ⟶ T) (hψ : ψ ≫ t = t')
    (s : SchemeHomOver pt gN) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (const t s) = const t' s
theorem

const_mul

L65 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const_mul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem const_mul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (s s' : SchemeHomOver pt gN) :
    const t (LN.mul pt s s') = LN.mul t (const t s) (const t s')
theorem

const_one

L69 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.const_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem const_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) :
    const t (LN.one pt) = LN.one t
theorem

inv_natural

L73 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.inv_natural
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem inv_natural {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (t' : T' ⟶ Spec (CommRingCat.of k)) (ψ : T' ⟶ T) (hψ : ψ ≫ t = t')
    (x : SchemeHomOver t gN) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (LN.inv t x) =
      LN.inv t' (GoodReductionJacobian.schemeHomOverComp ψ hψ x)
def

transl

L86 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.transl
Documentation

Translation by a rational point.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def transl (s : SchemeHomOver pt gN) : N ⟶ N
theorem

comp_transl

L89 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.comp_transl
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem comp_transl {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (x : SchemeHomOver t gN)
    (s : SchemeHomOver pt gN) : x.1 ≫ transl LN s = (LN.mul t (const t s) x).1
theorem

transl_one

L100 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.transl_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem transl_one : transl LN (LN.one pt) = 𝟙 N
theorem

transl_comp

L105 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.transl_comp
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem transl_comp (s s' : SchemeHomOver pt gN) :
    transl LN s ≫ transl LN s' = transl LN (LN.mul pt s' s)
instance

isIso_transl

L111 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIso_transl
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
instance isIso_transl (s : SchemeHomOver pt gN) : IsIso (transl LN s)
abbrev

clpt

L120 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.clpt
Documentation

The image of the unique closed point under a rational point.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
abbrev clpt (x : SchemeHomOver pt gN) : N
theorem

transl_clpt

L122 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.transl_clpt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem transl_clpt (x s : SchemeHomOver pt gN) :
    transl LN s (clpt x) = clpt (LN.mul pt s x)
theorem

range_coe_eq

L129 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_coe_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_coe_eq (x : SchemeHomOver pt gN) : Set.range x.1 = {clpt x}
def

invN

L138 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.invN
Documentation

The inversion morphism of the relative group law.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def invN : N ⟶ N
theorem

comp_invN

L140 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.comp_invN
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem comp_invN {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (x : SchemeHomOver t gN) :
    x.1 ≫ invN LN = (LN.inv t x).1
theorem

invN_invN

L149 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.invN_invN
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem invN_invN : invN LN ≫ invN LN = 𝟙 N
instance

isIso_invN

L156 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIso_invN
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
instance isIso_invN : IsIso (invN LN)
theorem

invN_clpt

L158 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.invN_clpt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Maps
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem invN_clpt (x : SchemeHomOver pt gN) : invN LN (clpt x) = clpt (LN.inv pt x)
theorem

image_mem_irreducibleComponents

L168 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.image_mem_irreducibleComponents
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
Lean source · statement
theorem image_mem_irreducibleComponents (h : α ≃ₜ β) {Z : Set α}
    (hZ : Z ∈ irreducibleComponents α) : h '' Z ∈ irreducibleComponents β
abbrev

redSub

L188 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.redSub
Documentation

The reduced closed subscheme associated to a closed subset.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
abbrev redSub (Z : Closeds N) : Scheme.{u}
abbrev

redι

L191 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.redι
Documentation

The inclusion of the reduced closed subscheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
abbrev redι (Z : Closeds N) : redSub Z ⟶ N
instance

isReduced_redSub

L193 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isReduced_redSub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
instance isReduced_redSub (Z : Closeds N) : IsReduced (redSub Z)
theorem

range_redι

L196 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_redι
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem range_redι (Z : Closeds N) : Set.range (redι Z) = (Z : Set N)
def

redLift

L201 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.redLift
Documentation

Factor a morphism from a reduced scheme through a closed reduced subscheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def redLift (Z : Closeds N) {T : Scheme.{u}} [IsReduced T] (f : T ⟶ N)
    (hf : Set.range f ⊆ Z) : T ⟶ redSub Z
theorem

redLift_ι

L208 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.redLift_ι
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem redLift_ι (Z : Closeds N) {T : Scheme.{u}} [IsReduced T] (f : T ⟶ N)
    (hf : Set.range f ⊆ Z) : redLift Z f hf ≫ redι Z = f
theorem

irreducibleSpace_redSub

L212 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.irreducibleSpace_redSub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem irreducibleSpace_redSub {Z : Closeds N} (hZ : IsIrreducible (Z : Set N)) :
    IrreducibleSpace (redSub Z)
theorem

isIntegral_redSub

L220 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIntegral_redSub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem isIntegral_redSub {Z : Closeds N} (hZ : IsIrreducible (Z : Set N)) :
    IsIntegral (redSub Z)
def

ratLift

L226 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ratLift
Documentation

Lift a rational point into its closed reduced subscheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def ratLift (Z : Closeds N) (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) gN)
    (hs : clpt s ∈ (Z : Set N)) :
    Spec (CommRingCat.of k) ⟶ redSub Z
theorem

ratLift_ι

L231 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ratLift_ι
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem ratLift_ι (Z : Closeds N) (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) gN)
    (hs : clpt s ∈ (Z : Set N)) : ratLift Z s hs ≫ redι Z = s.1
theorem

ratLift_over

L235 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ratLift_over
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem ratLift_over (Z : Closeds N) (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) gN)
    (hs : clpt s ∈ (Z : Set N)) : ratLift Z s hs ≫ redι Z ≫ gN = 𝟙 _
def

mulMap

L249 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.mulMap
Documentation

The multiplication morphism restricted to two reduced closed subschemes.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Mul
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def mulMap (C₁ C₂ : Closeds N) : pullback (redι C₁ ≫ gN) (redι C₂ ≫ gN) ⟶ N
theorem

lift_mulMap

L254 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.lift_mulMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Mul
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · full declaration
theorem lift_mulMap (C₁ C₂ : Closeds N) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (a : T ⟶ redSub C₁) (b : T ⟶ redSub C₂) (ha : a ≫ redι C₁ ≫ gN = t)
    (hb : b ≫ redι C₂ ≫ gN = t) :
    pullback.lift a b (ha.trans hb.symm) ≫ mulMap LN C₁ C₂ =
      (LN.mul t ⟨a ≫ redι C₁, by simpa using ha⟩ ⟨b ≫ redι C₂, by simpa using hb⟩).1 := by
  have hψ : pullback.lift a b (ha.trans hb.symm) ≫
      (pullback.fst (redι C₁ ≫ gN) (redι C₂ ≫ gN) ≫ redι C₁ ≫ gN) = t := by
    rw [pullback.lift_fst_assoc, ha]
  have hnat := LN.mul_natural _ t (pullback.lift a b (ha.trans hb.symm)) hψ
    ⟨pullback.fst _ _ ≫ redι C₁, by simp⟩
    ⟨pullback.snd _ _ ≫ redι C₂, by simpa using pullback.condition.symm⟩
  have h1 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.fst _ _ ≫ redι C₁, by simp⟩ : SchemeHomOver _ gN) =
      ⟨a ≫ redι C₁, by simpa using ha⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_fst])
  have h2 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.snd _ _ ≫ redι C₂, by simpa using pullback.condition.symm⟩ :
        SchemeHomOver _ gN) =
      ⟨b ≫ redι C₂, by simpa using hb⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_snd])
  rw [h1, h2] at hnat
  exact congrArg Subtype.val hnat
theorem

one_mem_range_mulMap

L279 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.one_mem_range_mulMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Mul
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem one_mem_range_mulMap (C₁ C₂ : Closeds N) (e₁ : clpt (LN.one pt) ∈ (C₁ : Set N))
    (e₂ : clpt (LN.one pt) ∈ (C₂ : Set N)) :
    clpt (LN.one pt) ∈ Set.range (mulMap LN C₁ C₂)
instance

isIntegral_pullback_redι

L297 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIntegral_pullback_redι
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Mul
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [IsAlgClosed k] [LocallyOfFiniteType gN]
Lean source · statement
instance isIntegral_pullback_redι (C₁ C₂ : Closeds N) [Fact (IsIrreducible (C₁ : Set N))]
    [Fact (IsIrreducible (C₂ : Set N))] : IsIntegral (pullback (redι C₁ ≫ gN) (redι C₂ ≫ gN))
theorem

isIrreducible_range_mulMap

L306 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIrreducible_range_mulMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Mul
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [IsAlgClosed k] [LocallyOfFiniteType gN]
Lean source · statement
theorem isIrreducible_range_mulMap (C₁ C₂ : Closeds N) (h₁ : IsIrreducible (C₁ : Set N))
    (h₂ : IsIrreducible (C₂ : Set N)) : IsIrreducible (Set.range (mulMap LN C₁ C₂))
def

idComp

L323 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.idComp
Documentation

The closed connected component of the identity.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def idComp : Closeds G
theorem

idComp_mem

L327 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.idComp_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
omit [IsAlgClosed k] [LocallyOfFiniteType f] in
Lean source · statement
theorem idComp_mem : (idComp L : Set G) ∈ irreducibleComponents G
theorem

one_mem_idComp

L331 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.one_mem_idComp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
omit [IsAlgClosed k] [LocallyOfFiniteType f] in
Lean source · statement
theorem one_mem_idComp : clpt (L.one pt) ∈ (idComp L : Set G)
theorem

isIrreducible_idComp

L335 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isIrreducible_idComp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
omit [IsAlgClosed k] [LocallyOfFiniteType f] in
Lean source · statement
theorem isIrreducible_idComp : IsIrreducible (idComp L : Set G)
theorem

eq_idComp_of_one_mem

L338 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.eq_idComp_of_one_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem eq_idComp_of_one_mem {Z : Set G} (hZ : Z ∈ irreducibleComponents G)
    (he : clpt (L.one pt) ∈ Z) : Z = idComp L
theorem

subset_idComp_of_isIrreducible

L343 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.subset_idComp_of_isIrreducible
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem subset_idComp_of_isIrreducible {W : Set G} (hW : IsIrreducible W)
    (he : clpt (L.one pt) ∈ W) : W ⊆ idComp L
theorem

exists_clpt_mem_of_isClosed

L349 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.exists_clpt_mem_of_isClosed
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem exists_clpt_mem_of_isClosed {Z : Set G} (hZ : IsClosed Z) (hne : Z.Nonempty) :
    ∃ s : SchemeHomOver pt f, clpt s ∈ Z
theorem

disjoint_idComp_of_ne

L359 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.disjoint_idComp_of_ne
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem disjoint_idComp_of_ne {Z : Set G} (hZ : Z ∈ irreducibleComponents G) (hne : Z ≠ idComp L) :
    Disjoint Z (idComp L : Set G)
theorem

finite_irreducibleComponents

L374 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.finite_irreducibleComponents
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
include f in
omit [IsAlgClosed k] in
Lean source · statement
theorem finite_irreducibleComponents : (irreducibleComponents G).Finite
theorem

compl_idComp_eq

L381 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.compl_idComp_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
omit [QuasiCompact f] in
Lean source · statement
theorem compl_idComp_eq :
    (idComp L : Set G)ᶜ = ⋃ Z ∈ {Z ∈ irreducibleComponents G | Z ≠ idComp L}, Z
theorem

isOpen_idComp

L394 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isOpen_idComp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
theorem isOpen_idComp : IsOpen (idComp L : Set G)
theorem

isClopen_idComp

L400 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isClopen_idComp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
theorem isClopen_idComp : IsClopen (idComp L : Set G)
def

U₀

L403 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.U₀
Documentation

The identity component as an open subset.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
def U₀ : G.Opens
abbrev

G₀

L406 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.G₀
Documentation

The open subscheme defined by the identity component.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
abbrev G₀ : Scheme.{u}
abbrev

ι₀

L409 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ι₀
Documentation

The inclusion of the identity component.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
abbrev ι₀ : G₀ L ⟶ G
abbrev

f₀

L412 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.f₀
Documentation

The structure morphism of the identity component.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
abbrev f₀ : G₀ L ⟶ Spec (CommRingCat.of k)
theorem

range_ι₀

L414 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_ι₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
theorem range_ι₀ : Set.range (ι₀ L) = (idComp L : Set G)
theorem

ι₀_apply_mem

L416 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ι₀_apply_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
theorem ι₀_apply_mem (a : G₀ L) : ι₀ L a ∈ (idComp L : Set G)
instance

irreducibleSpace_G₀

L419 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.irreducibleSpace_G₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
instance irreducibleSpace_G₀ : IrreducibleSpace (G₀ L)
instance

isClosedImmersion_ι₀

L425 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isClosedImmersion_ι₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
instance isClosedImmersion_ι₀ : IsClosedImmersion (ι₀ L)
theorem

range_ι₀_eq_connectedComponent

L428 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_ι₀_eq_connectedComponent
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section IdComp
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [QuasiCompact f]
Lean source · statement
theorem range_ι₀_eq_connectedComponent :
    Set.range (ι₀ L) = connectedComponent (clpt (L.one pt))
def

toG

L446 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG
Documentation

View a point of the identity component as a point of the ambient group.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def toG {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (x : SchemeHomOver t (f₀ L)) :
    SchemeHomOver t f
theorem

toG_coe

L450 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_coe
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_coe {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (x : SchemeHomOver t (f₀ L)) :
    (toG L x).1 = x.1 ≫ ι₀ L
theorem

toG_injective

L453 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_injective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_injective {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} :
    Function.Injective (toG L (T := T) (t := t))
theorem

toG_transition

L458 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_transition
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_transition {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₀ L)) :
    toG L (GoodReductionJacobian.schemeHomOverComp ψ hψ x) =
      GoodReductionJacobian.schemeHomOverComp ψ hψ (toG L x)
def

liftPt

L466 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.liftPt
Documentation

Lift a point whose image lies in the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def liftPt {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (y : SchemeHomOver t f)
    (hy : Set.range y.1 ⊆ (idComp L : Set G)) : SchemeHomOver t (f₀ L)
theorem

toG_liftPt

L471 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_liftPt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_liftPt {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (y : SchemeHomOver t f)
    (hy : Set.range y.1 ⊆ (idComp L : Set G)) : toG L (liftPt L y hy) = y
def

M

L476 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.M
Documentation

Multiplication of two points in the identity component, viewed in the ambient scheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def M : pullback (f₀ L) (f₀ L) ⟶ G
theorem

lift_M

L481 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.lift_M
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · full declaration
theorem lift_M {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (a b : T ⟶ G₀ L) (ha : a ≫ f₀ L = t) (hb : b ≫ f₀ L = t) :
    pullback.lift a b (ha.trans hb.symm) ≫ M L =
      (L.mul t ⟨a ≫ ι₀ L, by simpa using ha⟩ ⟨b ≫ ι₀ L, by simpa using hb⟩).1 := by
  have hψ : pullback.lift a b (ha.trans hb.symm) ≫ (pullback.fst (f₀ L) (f₀ L) ≫ f₀ L) = t := by
    rw [pullback.lift_fst_assoc, ha]
  have hnat := L.mul_natural _ t (pullback.lift a b (ha.trans hb.symm)) hψ
    ⟨pullback.fst _ _ ≫ ι₀ L, by simp⟩
    ⟨pullback.snd _ _ ≫ ι₀ L, by simpa using pullback.condition.symm⟩
  have h1 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.fst _ _ ≫ ι₀ L, by simp⟩ : SchemeHomOver _ f) =
      ⟨a ≫ ι₀ L, by simpa using ha⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_fst])
  have h2 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.snd _ _ ≫ ι₀ L, by simpa using pullback.condition.symm⟩ : SchemeHomOver _ f) =
      ⟨b ≫ ι₀ L, by simpa using hb⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_snd])
  rw [h1, h2] at hnat
  exact congrArg Subtype.val hnat
abbrev

A

L504 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.A
Documentation

The reduced closed subscheme underlying the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
abbrev A : Scheme.{u}
abbrev

ιA

L507 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.ιA
Documentation

The closed inclusion of the reduced identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
abbrev ιA : A L ⟶ G
def

j

L510 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.j
Documentation

The map from the reduced identity component to the open identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def j : A L ⟶ G₀ L
theorem

j_ι₀

L513 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.j_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem j_ι₀ : j L ≫ ι₀ L = ιA L
theorem

range_j

L515 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_j
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_j : Set.range (j L) = Set.univ
def

φ

L523 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.φ
Documentation

The induced map on products of reduced and open identity components.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def φ : pullback (ιA L ≫ f) (ιA L ≫ f) ⟶ pullback (f₀ L) (f₀ L)
theorem

range_φ

L526 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_φ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_φ : Set.range (φ L) = Set.univ
theorem

φ_M

L530 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.φ_M
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem φ_M : φ L ≫ M L = mulMap L (idComp L) (idComp L)
theorem

range_M_subset

L550 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_M_subset
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_M_subset : Set.range (M L) ⊆ (idComp L : Set G)
theorem

range_mul_toG_subset

L558 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_mul_toG_subset
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_mul_toG_subset {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (x y : SchemeHomOver t (f₀ L)) :
    Set.range (L.mul t (toG L x) (toG L y)).1 ⊆ (idComp L : Set G)
theorem

range_one_subset

L567 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_one_subset
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
omit [QuasiCompact f] [IsAlgClosed k] [LocallyOfFiniteType f] in
Lean source · statement
theorem range_one_subset {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) :
    Set.range (L.one t).1 ⊆ (idComp L : Set G)
theorem

range_ι₀_invN_subset

L574 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_ι₀_invN_subset
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_ι₀_invN_subset : Set.range (ι₀ L ≫ invN L) ⊆ (idComp L : Set G)
theorem

range_inv_toG_subset

L588 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.range_inv_toG_subset
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem range_inv_toG_subset {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (x : SchemeHomOver t (f₀ L)) :
    Set.range (L.inv t (toG L x)).1 ⊆ (idComp L : Set G)
def

mulPt

L595 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.mulPt
Documentation

Multiplication of points in the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def mulPt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t (f₀ L)) :
    SchemeHomOver t (f₀ L)
theorem

toG_mulPt

L599 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_mulPt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_mulPt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (x y : SchemeHomOver t (f₀ L)) :
    toG L (mulPt L t x y) = L.mul t (toG L x) (toG L y)
def

onePt

L605 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.onePt
Documentation

The identity point in the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def onePt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) : SchemeHomOver t (f₀ L)
theorem

toG_onePt

L608 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_onePt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_onePt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) :
    toG L (onePt L t) = L.one t
def

invPt

L613 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.invPt
Documentation

Inversion of points in the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
def invPt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x : SchemeHomOver t (f₀ L)) :
    SchemeHomOver t (f₀ L)
theorem

toG_invPt

L617 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_invPt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_invPt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (x : SchemeHomOver t (f₀ L)) : toG L (invPt L t x) = L.inv t (toG L x)
def

law₀

L622 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.law₀
Documentation

The relative group law induced on the identity component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · full declaration
def law₀ : RelativeGroupLaw k (f₀ L) where
  mul t x y := mulPt L t x y
  one t := onePt L t
  inv t x := invPt L t x
  mul_assoc t x y z := by
    apply toG_injective L
    simp only [toG_mulPt]
    exact L.mul_assoc t _ _ _
  one_mul t x := by
    apply toG_injective L
    simp only [toG_mulPt, toG_onePt]
    exact L.one_mul t _
  mul_one t x := by
    apply toG_injective L
    simp only [toG_mulPt, toG_onePt]
    exact L.mul_one t _
  inv_mul_cancel t x := by
    apply toG_injective L
    simp only [toG_mulPt, toG_invPt, toG_onePt]
    exact L.inv_mul_cancel t _
  mul_natural t t' ψ hψ x y := by
    apply toG_injective L
    rw [toG_transition]
    simp only [toG_mulPt]
    rw [L.mul_natural t t' ψ hψ, toG_transition, toG_transition]
theorem

toG_law₀_mul

L648 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.toG_law₀_mul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem toG_law₀_mul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (x y : SchemeHomOver t (f₀ L)) :
    toG L ((law₀ L).mul t x y) = L.mul t (toG L x) (toG L y)
theorem

hom_ι₀

L653 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.hom_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem hom_ι₀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t (f₀ L)) :
    NeronModelInfra.schemeHomOverComp ((law₀ L).mul t x y) (⟨ι₀ L, rfl⟩ : SchemeHomOver (f₀ L) f) =
      L.mul t (NeronModelInfra.schemeHomOverComp x (⟨ι₀ L, rfl⟩ : SchemeHomOver (f₀ L) f))
        (NeronModelInfra.schemeHomOverComp y (⟨ι₀ L, rfl⟩ : SchemeHomOver (f₀ L) f))
theorem

isCommutative_law₀

L659 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.isCommutative_law₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section Law
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem isCommutative_law₀ (hc : L.IsCommutative) : (law₀ L).IsCommutative
theorem

clpt_mul_inv_mem_idComp

L675 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.clpt_mul_inv_mem_idComp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section FiniteIndex
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
omit [QuasiCompact f] in
Lean source · statement
theorem clpt_mul_inv_mem_idComp (x s : SchemeHomOver pt f) {Z : Set G}
    (hZ : Z ∈ irreducibleComponents G) (hx : clpt x ∈ Z) (hs : clpt s ∈ Z) :
    clpt (L.mul pt (L.inv pt s) x) ∈ (idComp L : Set G)
theorem

exists_finite_cosets

L692 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.IdentityComponentFiniteIndex.P2mIdentityComponent.exists_finite_cosets
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace IdentityComponentFiniteIndex
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdentityComponent
section FiniteIndex
variable {k : Type u} [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
Lean source · statement
theorem exists_finite_cosets :
    ∃ S : Set (SchemeHomOver pt f), S.Finite ∧
      ∀ x : SchemeHomOver pt f, ∃ s ∈ S, ∃ a : SchemeHomOver pt (f₀ L),
        x = L.mul pt s (NeronModelInfra.schemeHomOverComp a (⟨ι₀ L, rfl⟩ : SchemeHomOver (f₀ L) f))
theorem

exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex

L738 ↗
GoodReductionJacobian.RelativeGroupLaw.exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex
Source context 6 commands

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

section ProofImplementation
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open IdentityComponentFiniteIndex.P2mIdentityComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
Lean source · statement
theorem exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex
    (k : Type u) [Field k] [IsAlgClosed k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
    [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f) :
    ∃ (G₀ : Scheme.{u}) (i : G₀ ⟶ G) (L₀ : RelativeGroupLaw k (i ≫ f)),
      IsOpenImmersion i ∧ IsClosedImmersion i ∧ IrreducibleSpace G₀ ∧
      Set.range i =
        connectedComponent ((L.one (𝟙 (Spec (CommRingCat.of k)))).1 (IsLocalRing.closedPoint k)) ∧
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (x y : SchemeHomOver t (i ≫ f)),
        NeronModelInfra.schemeHomOverComp (L₀.mul t x y) (⟨i, rfl⟩ : SchemeHomOver (i ≫ f) f) =
          L.mul t (NeronModelInfra.schemeHomOverComp x (⟨i, rfl⟩ : SchemeHomOver (i ≫ f) f))
            (NeronModelInfra.schemeHomOverComp y (⟨i, rfl⟩ : SchemeHomOver (i ≫ f) f))) ∧
      (L.IsCommutative → L₀.IsCommutative) ∧
      ∃ S : Set (SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) f), S.Finite ∧
        ∀ x : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) f,
          ∃ s ∈ S, ∃ a : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) (i ≫ f),
            x = L.mul (𝟙 (Spec (CommRingCat.of k))) s
              (NeronModelInfra.schemeHomOverComp a (⟨i, rfl⟩ : SchemeHomOver (i ≫ f) f))

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