Module

RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem

40 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law eq of mem irreducible Components of apply closed Point mem

Imports5

Imported by2

def

const

L45 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L49 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L52 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L55 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L61 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L65 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L69 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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)

theorem

const_inv

L81 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.const_inv

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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_inv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (s : SchemeHomOver pt gN) :
    const t (LN.inv pt s) = LN.inv t (const t s)

def

transl

L86 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

transl_over

L89 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.transl_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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_over (s : SchemeHomOver pt gN) : transl LN s ≫ gN = gN

theorem

comp_transl

L92 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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_point

L103 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.transl_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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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 · full declaration

theorem transl_point {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of k)} (x : SchemeHomOver t gN)
    (s : SchemeHomOver pt gN) :
    (⟨x.1 ≫ transl LN s, by rw [Category.assoc, transl_over, x.2]⟩ : SchemeHomOver t gN) =
      LN.mul t (const t s) x :=
  Subtype.ext (comp_transl LN x s)

theorem

transl_one

L109 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L114 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L120 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L129 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

L131 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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

transl_clpt_one

L138 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.transl_clpt_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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
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_one (s : SchemeHomOver pt gN) :
    transl LN s (clpt (LN.one pt)) = clpt s

theorem

image_mem_irreducibleComponents

L148 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.image_mem_irreducibleComponents

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]

Lean source · statement

theorem image_mem_irreducibleComponents (h : α ≃ₜ β) {Z : Set α}
    (hZ : Z ∈ irreducibleComponents α) : h '' Z ∈ irreducibleComponents β

theorem

eq_of_mem_irreducibleComponents_of_subset

L159 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.eq_of_mem_irreducibleComponents_of_subset

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Topology
variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]

Lean source · statement

theorem eq_of_mem_irreducibleComponents_of_subset {Z W : Set α} (hZ : Z ∈ irreducibleComponents α)
    (hW : IsIrreducible W) (hZW : Z ⊆ W) : W = Z

abbrev

redSub

L172 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.redSub

Documentation

The reduced closed subscheme associated to a closed subset.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

abbrev redSub (Z : Closeds N) : Scheme.{u}

abbrev

redι

L175 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.redι

Documentation

The inclusion of the reduced closed subscheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

abbrev redι (Z : Closeds N) : redSub Z ⟶ N

instance

isReduced_redSub

L177 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.isReduced_redSub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

instance isReduced_redSub (Z : Closeds N) : IsReduced (redSub Z)

theorem

range_redι

L180 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.range_redι

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem range_redι (Z : Closeds N) : Set.range (redι Z) = (Z : Set N)

theorem

redι_apply_mem

L184 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.redι_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_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem redι_apply_mem (Z : Closeds N) (a : redSub Z) : redι Z a ∈ (Z : Set N)

def

redLift

L189 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.redLift

Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

def redLift (Z : Closeds N) {T : Scheme.{u}} [IsReduced T] (f : T ⟶ N)
    (hf : Set.range f ⊆ Z) : T ⟶ redSub Z

theorem

redLift_ι

L196 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.redLift_ι

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem redLift_ι (Z : Closeds N) {T : Scheme.{u}} [IsReduced T] (f : T ⟶ N)
    (hf : Set.range f ⊆ Z) : redLift Z f hf ≫ redι Z = f

theorem

irreducibleSpace_redSub

L200 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.irreducibleSpace_redSub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem irreducibleSpace_redSub {Z : Closeds N} (hZ : IsIrreducible (Z : Set N)) :
    IrreducibleSpace (redSub Z)

theorem

isIntegral_redSub

L208 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.isIntegral_redSub

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Component
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
open AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem isIntegral_redSub {Z : Closeds N} (hZ : IsIrreducible (Z : Set N)) :
    IsIntegral (redSub Z)

def

ratLift

L223 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.ratLift

Documentation

The rational point lifted to the reduced closed subscheme containing its image.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
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 ratLift (Z : Closeds N) (s : SchemeHomOver pt gN) (hs : clpt s ∈ (Z : Set N)) :
    Spec (CommRingCat.of k) ⟶ redSub Z

theorem

ratLift_ι

L230 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.ratLift_ι

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
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 ratLift_ι (Z : Closeds N) (s : SchemeHomOver pt gN) (hs : clpt s ∈ (Z : Set N)) :
    ratLift Z s hs ≫ redι Z = s.1

theorem

ratLift_over

L234 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.ratLift_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
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 ratLift_over (Z : Closeds N) (s : SchemeHomOver pt gN) (hs : clpt s ∈ (Z : Set N)) :
    ratLift Z s hs ≫ redι Z ≫ gN = 𝟙 _

def

mulMap

L239 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.mulMap

Documentation

The multiplication morphism restricted to two reduced closed subschemes.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))

Lean source · statement

def mulMap (C₁ C₂ : Closeds N) : pullback (redι C₁ ≫ gN) (redι C₂ ≫ gN) ⟶ N

theorem

lift_mulMap

L244 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.lift_mulMap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))

Lean source · full declaration

theorem lift_mulMap (C₁ C₂ : Closeds N) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k))
    (a : T ⟶ redSub C₁) (b : T ⟶ redSub C₂) (ha : a ≫ redι C₁ ≫ gN = t)
    (hb : b ≫ redι C₂ ≫ gN = t) :
    pullback.lift a b (ha.trans hb.symm) ≫ mulMap LN C₁ C₂ =
      (LN.mul t ⟨a ≫ redι C₁, by simpa using ha⟩ ⟨b ≫ redι C₂, by simpa using hb⟩).1 := by
  have hψ : pullback.lift a b (ha.trans hb.symm) ≫
      (pullback.fst (redι C₁ ≫ gN) (redι C₂ ≫ gN) ≫ redι C₁ ≫ gN) = t := by
    rw [pullback.lift_fst_assoc, ha]
  have hnat := LN.mul_natural _ t (pullback.lift a b (ha.trans hb.symm)) hψ
    ⟨pullback.fst _ _ ≫ redι C₁, by simp⟩
    ⟨pullback.snd _ _ ≫ redι C₂, by simpa using pullback.condition.symm⟩
  have h1 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.fst _ _ ≫ redι C₁, by simp⟩ : SchemeHomOver _ gN) =
      ⟨a ≫ redι C₁, by simpa using ha⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_fst])
  have h2 : GoodReductionJacobian.schemeHomOverComp (pullback.lift a b (ha.trans hb.symm)) hψ
      (⟨pullback.snd _ _ ≫ redι C₂, by simpa using pullback.condition.symm⟩ :
        SchemeHomOver _ gN) =
      ⟨b ≫ redι C₂, by simpa using hb⟩ :=
    Subtype.ext (by rw [GoodReductionJacobian.schemeHomOverComp_coe, ← Category.assoc,
      pullback.lift_snd])
  rw [h1, h2] at hnat
  exact congrArg Subtype.val hnat

theorem

subset_range_mulMap_left

L269 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.subset_range_mulMap_left

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
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 subset_range_mulMap_left (C₁ C₂ : Closeds N) (e₂ : clpt (LN.one pt) ∈ (C₂ : Set N)) :
    (C₁ : Set N) ⊆ Set.range (mulMap LN C₁ C₂)

theorem

subset_range_mulMap_right

L291 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.subset_range_mulMap_right

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
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 subset_range_mulMap_right (C₁ C₂ : Closeds N) (e₁ : clpt (LN.one pt) ∈ (C₁ : Set N)) :
    (C₂ : Set N) ⊆ Set.range (mulMap LN C₁ C₂)

theorem

isIrreducible_range_mulMap

L315 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.isIrreducible_range_mulMap

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [IsAlgClosed k] [LocallyOfFiniteType gN]

Lean source · statement

theorem isIrreducible_range_mulMap (C₁ C₂ : Closeds N) (h₁ : IsIrreducible (C₁ : Set N))
    (h₂ : IsIrreducible (C₂ : Set N)) : IsIrreducible (Set.range (mulMap LN C₁ C₂))

theorem

eq_of_one_mem

L326 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.eq_of_one_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [IsAlgClosed k] [LocallyOfFiniteType gN]

Lean source · statement

theorem eq_of_one_mem {Z₁ Z₂ : Set N} (h₁ : Z₁ ∈ irreducibleComponents N)
    (h₂ : Z₂ ∈ irreducibleComponents N) (e₁ : clpt (LN.one pt) ∈ Z₁)
    (e₂ : clpt (LN.one pt) ∈ Z₂) : Z₁ = Z₂

theorem

eq_of_clpt_mem

L340 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem.P2mGroupSchemeComponents.eq_of_clpt_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  TopologicalSpace
noncomputable section
universe u
namespace P2mGroupSchemeComponents
section Identity
variable {k : Type u} [Field k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
  (LN : RelativeGroupLaw k gN)
local notation "pt" => 𝟙 (Spec (CommRingCat.of k))
variable [IsAlgClosed k] [LocallyOfFiniteType gN]
include LN in

Lean source · statement

theorem eq_of_clpt_mem (x : SchemeHomOver pt gN) {Z Z' : Set N}
    (hZ : Z ∈ irreducibleComponents N) (hZ' : Z' ∈ irreducibleComponents N)
    (hx : clpt x ∈ Z) (hx' : clpt x ∈ Z') : Z = Z'

theorem

eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem

L373 ↗

GoodReductionJacobian.RelativeGroupLaw.eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
open P2mGroupSchemeComponents
namespace GoodReductionJacobian.RelativeGroupLaw

Lean source · statement

theorem eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem
    (k : Type u) [Field k] [IsAlgClosed k] {N : Scheme.{u}} {gN : N ⟶ Spec (CommRingCat.of k)}
    [LocallyOfFiniteType gN] (LN : RelativeGroupLaw k gN)
    (x : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) gN)
    {Z Z' : Set N} (hZ : Z ∈ irreducibleComponents N) (hZ' : Z' ∈ irreducibleComponents N)
    (hx : x.1 (IsLocalRing.closedPoint k) ∈ Z) (hx' : x.1 (IsLocalRing.closedPoint k) ∈ Z') :
    Z = Z'

Module documentation

Relative Group Law eq of mem irreducible Components of apply closed Point mem

Declarations