NYLL
Module

RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
93 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law exists is Open Immersion geometrically Connected range eq connected

Component

Imports62
Imported by3

Declarations

def

const

L103 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L107 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L110 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L113 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L119 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L123 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L127 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L140 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L143 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L154 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L159 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L165 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L174 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L176 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L183 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L192 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L194 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L203 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L210 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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

L212 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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)
abbrev

ePt

L217 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.ePt
Documentation

The underlying point of the identity section.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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 ePt : N
theorem

invN_ePt

L219 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.invN_ePt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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_ePt : invN LN (ePt LN) = ePt LN
theorem

transl_ePt

L223 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.transl_ePt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
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_ePt (s : SchemeHomOver pt gN) : transl LN s (ePt LN) = clpt s
theorem

homeomorph_image_connectedComponent

L232 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.homeomorph_image_connectedComponent
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
Lean source · statement
theorem homeomorph_image_connectedComponent (h : α ≃ₜ β) (x : α) :
    h '' connectedComponent x = connectedComponent (h x)
theorem

eq_connectedComponent_of_isClopen_of_isPreconnected

L241 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.eq_connectedComponent_of_isClopen_of_isPreconnected
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
Lean source · statement
theorem eq_connectedComponent_of_isClopen_of_isPreconnected {s : Set α} (hs : IsClopen s)
    (hc : IsPreconnected s) {x : α} (hx : x ∈ s) : s = connectedComponent x
theorem

isOpen_connectedComponent_of_finite_irreducibleComponents

L245 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isOpen_connectedComponent_of_finite_irreducibleComponents
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
Lean source · statement
theorem isOpen_connectedComponent_of_finite_irreducibleComponents
    (hfin : (irreducibleComponents α).Finite) (x : α) : IsOpen (connectedComponent x)
def

idC

L277 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.idC
Documentation

The connected component containing the identity point.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 idC : Set G
theorem

ePt_mem_idC

L279 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.ePt_mem_idC
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
theorem ePt_mem_idC : ePt L ∈ idC L
theorem

finite_irreducibleComponents

L281 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.finite_irreducibleComponents
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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))
include f in
Lean source · statement
theorem finite_irreducibleComponents : (irreducibleComponents G).Finite
theorem

isOpen_idC

L291 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isOpen_idC
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 isOpen_idC : IsOpen (idC L)
theorem

isClosed_idC

L295 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isClosed_idC
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
theorem isClosed_idC : IsClosed (idC L)
theorem

isClopen_idC

L297 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isClopen_idC
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 isClopen_idC : IsClopen (idC L)
theorem

isConnected_idC

L299 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isConnected_idC
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
theorem isConnected_idC : _root_.IsConnected (idC L)
def

U₀

L302 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.U₀
Documentation

The identity component as an open subset of the group scheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 U₀ : G.Opens
abbrev

G₀

L305 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.G₀
Documentation

The open subscheme defined by 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 G₀ : Scheme.{u}
abbrev

ι₀

L308 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.ι₀
Documentation

The inclusion of 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 ι₀ : G₀ L ⟶ G
abbrev

f₀

L311 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.f₀
Documentation

The structure morphism of 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 f₀ : G₀ L ⟶ Spec (CommRingCat.of k)
theorem

range_ι₀

L313 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.range_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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) = idC L
theorem

ι₀_apply_mem

L315 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.ι₀_apply_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 ι₀_apply_mem (a : G₀ L) : ι₀ L a ∈ idC L
instance

isClosedImmersion_ι₀

L318 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isClosedImmersion_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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
instance isClosedImmersion_ι₀ : IsClosedImmersion (ι₀ L)
instance

connectedSpace_G₀

L321 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.connectedSpace_G₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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
instance connectedSpace_G₀ : ConnectedSpace (G₀ L)
def

liftPt

L328 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.liftPt
Documentation

The lift of 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 ⊆ idC L) : SchemeHomOver t (f₀ L)
theorem

liftPt_coe_ι₀

L333 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.liftPt_coe_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 liftPt_coe_ι₀ {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (y : SchemeHomOver t f)
    (hy : Set.range y.1 ⊆ idC L) : (liftPt L y hy).1 ≫ ι₀ L = y.1
def

e₀

L338 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.e₀
Documentation

The identity section lifted to 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section IdComp
variable {k : Type u} [Field 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 e₀ : SchemeHomOver pt (f₀ L)
theorem

one_comp_eq

L353 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.one_comp_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem one_comp_eq (L : RelativeGroupLaw k f) {T : Scheme.{u}} (s : T ⟶ Spec (CommRingCat.of k)) :
    (L.one s).1 = s ≫ (L.one pt).1
theorem

fst_ePt_baseChange

L357 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.fst_ePt_baseChange
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem fst_ePt_baseChange :
    pullback.fst f t (ePt (L.baseChange t)) = ePt L
theorem

subsingleton_pullback_one_fst

L371 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.subsingleton_pullback_one_fst
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem subsingleton_pullback_one_fst :
    Subsingleton ↥(pullback (L.one pt).1 (pullback.fst f t))
theorem

eq_ePt_of_fst_eq

L384 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.eq_ePt_of_fst_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem eq_ePt_of_fst_eq {z : ↥(pullback f t)} (hz : pullback.fst f t z = ePt L) :
    z = ePt (L.baseChange t)
theorem

isClopen_preimage_idC

L398 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isClopen_preimage_idC
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem isClopen_preimage_idC [LocallyOfFiniteType f] [QuasiCompact f] :
    IsClopen (pullback.fst f t ⁻¹' idC L)
theorem

ePt_baseChange_mem_preimage

L402 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.ePt_baseChange_mem_preimage
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section BaseChange
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k))
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
Lean source · statement
theorem ePt_baseChange_mem_preimage [LocallyOfFiniteType f] [QuasiCompact f] :
    ePt (L.baseChange t) ∈ pullback.fst f t ⁻¹' idC L
def

tb

L421 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.tb
Documentation

The spectrum map associated with extension of the base field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section AlgClosure
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
variable (k K) in
Lean source · statement
def tb : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k)
instance

isIntegralHom_tb

L424 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isIntegralHom_tb
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section AlgClosure
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
variable (k K) in
Lean source · statement
instance isIntegralHom_tb : IsIntegralHom (tb k K)
instance

surjective_tb

L429 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.surjective_tb
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section AlgClosure
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
variable (k K) in
Lean source · statement
instance surjective_tb : Surjective (tb k K)
theorem

exists_mem_image_connectedComponent

L433 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.exists_mem_image_connectedComponent
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section AlgClosure
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
variable (k K) in
omit [QuasiCompact f] [Algebra.IsIntegral k K] in
Lean source · statement
theorem exists_mem_image_connectedComponent (y : ↥(pullback f (tb k K))) :
    ∃ s : SchemeHomOver ptK (pullback.snd f (tb k K)),
      y ∈ (transl (L.baseChange (tb k K)) s).homeomorph '' idC (L.baseChange (tb k K))
theorem

preimage_idC_eq_idC

L453 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.preimage_idC_eq_idC
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section AlgClosure
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
  {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
local notation "ptK" => 𝟙 (Spec (CommRingCat.of K))
variable (k K) in
Lean source · statement
theorem preimage_idC_eq_idC :
    pullback.fst f (tb k K) ⁻¹' idC L = idC (L.baseChange (tb k K))
theorem

isIrreducible_idC_of_isAlgClosed

L493 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isIrreducible_idC_of_isAlgClosed
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
open _root_.GoodReductionJacobian.RelativeGroupLaw in
Lean source · statement
theorem isIrreducible_idC_of_isAlgClosed {K : Type u} [Field K] [IsAlgClosed K] {G' : Scheme.{u}}
    {f' : G' ⟶ Spec (CommRingCat.of K)} [LocallyOfFiniteType f'] [QuasiCompact f']
    (L' : RelativeGroupLaw K f') : IsIrreducible (idC L')
theorem

irreducibleSpace_G₀_of_isAlgClosed

L504 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.irreducibleSpace_G₀_of_isAlgClosed
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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 irreducibleSpace_G₀_of_isAlgClosed {K : Type u} [Field K] [IsAlgClosed K]
    {G' : Scheme.{u}} {f' : G' ⟶ Spec (CommRingCat.of K)} [LocallyOfFiniteType f']
    [QuasiCompact f'] (L' : RelativeGroupLaw K f') : IrreducibleSpace (G₀ L')
theorem

geometricallyIrreducible_f₀_of_isAlgClosed

L513 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.geometricallyIrreducible_f₀_of_isAlgClosed
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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 geometricallyIrreducible_f₀_of_isAlgClosed {K : Type u} [Field K] [IsAlgClosed K]
    {G' : Scheme.{u}} {f' : G' ⟶ Spec (CommRingCat.of K)} [LocallyOfFiniteType f']
    [QuasiCompact f'] (L' : RelativeGroupLaw K f') : GeometricallyIrreducible (f₀ L')
theorem

geometricallyIrreducible_of_snd

L519 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.geometricallyIrreducible_of_snd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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 geometricallyIrreducible_of_snd {X : Scheme.{u}} (h : X ⟶ Spec (CommRingCat.of k))
    {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k)) [Surjective t]
    [hgi : GeometricallyIrreducible (pullback.snd h t)] : GeometricallyIrreducible h
theorem

range_snd_ι₀_fst

L553 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.range_snd_ι₀_fst
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
theorem range_snd_ι₀_fst :
    Set.range (pullback.snd (ι₀ L) (pullback.fst f (tb k K))) = idC (L.baseChange (tb k K))
def

isoG₀b

L561 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isoG₀b
Documentation

The comparison isomorphism identifying the base change of the identity component with the new 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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
def isoG₀b : pullback (ι₀ L) (pullback.fst f (tb k K)) ≅ G₀ (L.baseChange (tb k K))
theorem

isoG₀b_hom_ι₀

L565 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.isoG₀b_hom_ι₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
theorem isoG₀b_hom_ι₀ :
    (isoG₀b L (K := K)).hom ≫ ι₀ (L.baseChange (tb k K)) =
      pullback.snd (ι₀ L) (pullback.fst f (tb k K))
theorem

snd_f₀_tb_eq

L570 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.snd_f₀_tb_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
theorem snd_f₀_tb_eq :
    pullback.snd (f₀ L) (tb k K) =
      (pullbackRightPullbackFstIso f (tb k K) (ι₀ L)).inv ≫ (isoG₀b L (K := K)).hom ≫
        f₀ (L.baseChange (tb k K))
theorem

geometricallyIrreducible_snd_f₀_tb

L576 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.geometricallyIrreducible_snd_f₀_tb
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
theorem geometricallyIrreducible_snd_f₀_tb :
    GeometricallyIrreducible (pullback.snd (f₀ L) (tb k K))
instance

geometricallyIrreducible_f₀

L585 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.geometricallyIrreducible_f₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
instance geometricallyIrreducible_f₀ : GeometricallyIrreducible (f₀ L)
instance

geometricallyConnected_f₀

L589 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.geometricallyConnected_f₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
instance geometricallyConnected_f₀ : GeometricallyConnected (f₀ L)
instance

irreducibleSpace_G₀

L592 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Geometric
variable {k : Type u} [Field 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))
variable {K : Type u} [Field K] [IsAlgClosed K] [Algebra k K] [Algebra.IsIntegral k K]
Lean source · statement
instance irreducibleSpace_G₀ : IrreducibleSpace (G₀ L)
theorem

preimage_range_ι₀_eq

L602 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.preimage_range_ι₀_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Compat
variable {k : Type u} [Field k] {G : Scheme.{u}} {f : G ⟶ Spec (CommRingCat.of k)}
  [LocallyOfFiniteType f] [QuasiCompact f] (L : RelativeGroupLaw k f)
Lean source · statement
theorem preimage_range_ι₀_eq {K : Type u} [Field K]
    (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k)) :
    pullback.fst f t ⁻¹' Set.range (ι₀ L) = connectedComponent (ePt (L.baseChange t))
def

toG

L624 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L628 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L631 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L636 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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)
theorem

toG_liftPt

L643 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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 ⊆ idC L) : toG L (liftPt L y hy) = y
def

M

L648 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L653 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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
theorem

range_M_subset

L675 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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) ⊆ idC L
theorem

range_mul_toG_subset

L686 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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 ⊆ idC L
theorem

range_one_subset

L694 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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 [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
theorem range_one_subset {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) :
    Set.range (L.one t).1 ⊆ idC L
theorem

range_ι₀_invN_subset

L701 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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) ⊆ idC L
theorem

range_inv_toG_subset

L711 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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 ⊆ idC L
def

mulPt

L718 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L722 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L728 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L731 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L736 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L740 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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₀

L745 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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

L771 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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_ι₀

L776 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.hom_ι₀
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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₀

L782 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section Law
variable {k : Type u} [Field 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_idC

L798 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.clpt_mul_inv_mem_idC
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section FiniteIndex
variable {k : Type u} [Field 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 [LocallyOfFiniteType f] [QuasiCompact f] in
Lean source · statement
theorem clpt_mul_inv_mem_idC (x s : SchemeHomOver pt f) (hs : clpt s ∈ connectedComponent (clpt x))
  :
    clpt (L.mul pt (L.inv pt s) x) ∈ idC L
theorem

exists_finite_cosets

L816 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent.P2mIdCompField.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 RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mIdCompField
section FiniteIndex
variable {k : Type u} [Field 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_geometricallyConnected_range_eq_connectedComponent

L917 ↗
GoodReductionJacobian.RelativeGroupLaw.exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
Source context 20 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
attribute [local simp]
  P2mIdCompField.const_coe
attribute [local instance]
  P2mIdCompField.isIso_transl
attribute [local instance]
  P2mIdCompField.isIso_invN
attribute [local instance]
  P2mIdCompField.isClosedImmersion_ι₀
attribute [local instance]
  P2mIdCompField.connectedSpace_G₀
attribute [local simp]
  P2mIdCompField.liftPt_coe_ι₀
attribute [local instance]
  P2mIdCompField.isIntegralHom_tb
attribute [local instance]
  P2mIdCompField.surjective_tb
attribute [local instance]
  P2mIdCompField.geometricallyIrreducible_f₀
attribute [local instance]
  P2mIdCompField.geometricallyConnected_f₀
attribute [local instance]
  P2mIdCompField.irreducibleSpace_G₀
attribute [local simp]
  P2mIdCompField.toG_coe
attribute [local simp]
  P2mIdCompField.toG_liftPt
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent in
open P2mIdCompField in
Lean source · statement
theorem exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent
    (k : Type u) [Field 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₀ ∧
      GeometricallyIrreducible (i ≫ f) ∧ GeometricallyConnected (i ≫ f) ∧
      Set.range i =
        connectedComponent ((L.one (𝟙 (Spec (CommRingCat.of k)))).1 (IsLocalRing.closedPoint k)) ∧
      (∀ (K : Type u) [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of k)),
        pullback.fst f t ⁻¹' Set.range i =
          connectedComponent
            (((L.baseChange t).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.