NYLL
Module

KernelPair.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.KernelPair
39 declarations indexed from sourceView source ↗

Module documentation

Kernel Pair

Imports2
Imported by1

Declarations

def

IsHom

L37 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom
Documentation

A morphism over the base preserves the relative group multiplication on all points.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
Lean source · statement
def IsHom (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (ψ : SchemeHomOver f f') : Prop
theorem

mul

L46 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.mul
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
namespace IsHom
variable {G : RelativeGroupLaw R f} {G' : RelativeGroupLaw R f'} {G'' : RelativeGroupLaw R f''}
Lean source · statement
theorem mul {ψ : SchemeHomOver f f'} (h : IsHom G G' ψ) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f) :
    NeronModelInfra.schemeHomOverComp (G.mul t x y) ψ =
      G'.mul t (NeronModelInfra.schemeHomOverComp x ψ) (NeronModelInfra.schemeHomOverComp y ψ)
theorem

one

L52 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.one
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
namespace IsHom
variable {G : RelativeGroupLaw R f} {G' : RelativeGroupLaw R f'} {G'' : RelativeGroupLaw R f''}
Lean source · statement
theorem one {ψ : SchemeHomOver f f'} (h : IsHom G G' ψ) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) :
    NeronModelInfra.schemeHomOverComp (G.one t) ψ = G'.one t
theorem

inv

L63 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.inv
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
namespace IsHom
variable {G : RelativeGroupLaw R f} {G' : RelativeGroupLaw R f'} {G'' : RelativeGroupLaw R f''}
Lean source · statement
theorem inv {ψ : SchemeHomOver f f'} (h : IsHom G G' ψ) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t f) :
    NeronModelInfra.schemeHomOverComp (G.inv t x) ψ = G'.inv t (NeronModelInfra.schemeHomOverComp x
      ψ)
theorem

id

L74 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.id
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
namespace IsHom
variable {G : RelativeGroupLaw R f} {G' : RelativeGroupLaw R f'} {G'' : RelativeGroupLaw R f''}
Lean source · statement
theorem id (G : RelativeGroupLaw R f) : IsHom G G (NeronModelInfra.schemeHomOverId f)
theorem

comp

L78 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.comp
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
namespace IsHom
variable {G : RelativeGroupLaw R f} {G' : RelativeGroupLaw R f'} {G'' : RelativeGroupLaw R f''}
Lean source · statement
theorem comp {ψ : SchemeHomOver f f'} {χ : SchemeHomOver f' f''} (hψ : IsHom G G' ψ) (hχ : IsHom G'
  G'' χ) :
    IsHom G G'' (NeronModelInfra.schemeHomOverComp ψ χ)
theorem

fibreRestrictAlong

L88 ↗
GoodReductionJacobian.RelativeGroupLaw.IsHom.fibreRestrictAlong
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section IsHom
variable {R : Type u} [CommRing R] {A A' A'' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)} {f'' : A'' ⟶ Spec
    (CommRingCat.of R)}
Lean source · statement
theorem IsHom.fibreRestrictAlong {R' : Type u} [CommRing R'] (ι : Spec (CommRingCat.of R') ⟶ Spec
  (CommRingCat.of R))
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} {Gg : RelativeGroupLaw R g} {Gf :
      RelativeGroupLaw R f}
    {ψ : SchemeHomOver g f} (h : IsHom Gg Gf ψ) :
    IsHom (Gg.baseChange ι) (Gf.baseChange ι) (NeronModelInfra.fibreRestrictAlong ι f g ψ)
abbrev

kerPair

L109 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPair
Documentation

The fibre-product intersection of the kernels of two morphisms to the target group.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev kerPair (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f') : Scheme.{u}
abbrev

kerPairι

L114 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairι
Documentation

The canonical morphism from the intersection of the two kernels to the source scheme.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev kerPairι (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f') : kerPair G' φ ⟶ A
abbrev

kerPairStr

L120 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairStr
Documentation

The structure morphism of the intersection of the two kernels.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev kerPairStr (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f') :
    kerPair G' φ ⟶ Spec (CommRingCat.of R)
theorem

kerLeg_snd_eq

L126 ↗
GoodReductionJacobian.RelativeGroupLaw.kerLeg_snd_eq
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerLeg_snd_eq (i : Fin 2) :
    pullback.snd (φ i).1 (G'.one (𝟙 (Spec (CommRingCat.of R)))).1 =
      pullback.fst (φ i).1 (G'.one (𝟙 (Spec (CommRingCat.of R)))).1 ≫ f
theorem

kerPair_snd_fst

L135 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPair_snd_fst
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPair_snd_fst :
    pullback.snd (pullback.fst (φ 0).1 (G'.one (𝟙 (Spec (CommRingCat.of R)))).1)
        (pullback.fst (φ 1).1 (G'.one (𝟙 (Spec (CommRingCat.of R)))).1) ≫
      pullback.fst (φ 1).1 (G'.one (𝟙 (Spec (CommRingCat.of R)))).1 = kerPairι G' φ
theorem

kerPairι_comp

L141 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairι_comp
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairι_comp (i : Fin 2) :
    kerPairι G' φ ≫ (φ i).1 = kerPairStr G' φ ≫ (G'.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

one_coe_eq

L153 ↗
GoodReductionJacobian.RelativeGroupLaw.one_coe_eq
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem one_coe_eq {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    (G'.one t).1 = t ≫ (G'.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

kerPairι_mem

L158 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairι_mem
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · full declaration
theorem kerPairι_mem {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (z : SchemeHomOver t
  (kerPairStr G' φ))
    (i : Fin 2) :
    NeronModelInfra.schemeHomOverComp (⟨z.1 ≫ kerPairι G' φ,
      by rw [Category.assoc]; exact z.2⟩ : SchemeHomOver t f)
      (φ i) = G'.one t := by
  apply Subtype.ext
  rw [NeronModelInfra.schemeHomOverComp_coe, one_coe_eq, Category.assoc, kerPairι_comp, ←
    Category.assoc, z.2]
def

kerPairLift

L169 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairLift
Documentation

The lift to the kernel intersection of a point sent to the identity by both morphisms.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
def kerPairLift {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x : SchemeHomOver t f)
    (hx : ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t) : T ⟶ kerPair G' φ
theorem

kerPairLift_ι

L176 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairLift_ι
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairLift_ι {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x : SchemeHomOver t f)
    (hx : ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t) :
    kerPairLift G' φ x hx ≫ kerPairι G' φ = x.1
def

kerPairPointEquiv

L185 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv
Documentation

The equivalence between points of the kernel intersection and points satisfying both kernel equations.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · full declaration
def kerPairPointEquiv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    SchemeHomOver t (kerPairStr G' φ) ≃
      {x : SchemeHomOver t f // ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t} where
  toFun z := ⟨⟨z.1 ≫ kerPairι G' φ, by rw [Category.assoc]; exact z.2⟩, kerPairι_mem G' φ z⟩
  invFun x := ⟨kerPairLift G' φ x.1 x.2, by
    change _ ≫ kerPairι G' φ ≫ f = t
    rw [← Category.assoc, kerPairLift_ι]; exact x.1.2⟩
  left_inv z := by
    have hz : z.1 ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ f = t := by
      have := z.2; simp only [Category.assoc] at this; exact this
    apply Subtype.ext
    change kerPairLift G' φ ⟨z.1 ≫ kerPairι G' φ,
      by rw [Category.assoc]; exact z.2⟩ (kerPairι_mem G' φ z) = z.1
    apply pullback.hom_ext
    · rw [kerPairLift, pullback.lift_fst]
      apply pullback.hom_ext
      · rw [pullback.lift_fst]
        change z.1 ≫ kerPairι G' φ = (z.1 ≫ pullback.fst _ _) ≫ pullback.fst _ _
        rw [Category.assoc]
      · rw [pullback.lift_snd, kerLeg_snd_eq, Category.assoc, hz]
    · rw [kerPairLift, pullback.lift_snd]
      apply pullback.hom_ext
      · rw [pullback.lift_fst]
        change z.1 ≫ kerPairι G' φ = (z.1 ≫ pullback.snd _ _) ≫ pullback.fst _ _
        rw [Category.assoc, kerPair_snd_fst]
      · rw [pullback.lift_snd, kerLeg_snd_eq, Category.assoc, kerPair_snd_fst_assoc, hz]
  right_inv x := by
    apply Subtype.ext
    apply Subtype.ext
    exact kerPairLift_ι G' φ x.1 x.2
theorem

kerPairPointEquiv_apply_coe_coe

L216 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_apply_coe_coe
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairPointEquiv_apply_coe_coe {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (z : SchemeHomOver t (kerPairStr G' φ)) :
    ((kerPairPointEquiv G' φ t z).1).1 = z.1 ≫ kerPairι G' φ
theorem

kerPairPointEquiv_symm_apply_coe

L221 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_symm_apply_coe
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairPointEquiv_symm_apply_coe {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (x : {x : SchemeHomOver t f // ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t}) :
    ((kerPairPointEquiv G' φ t).symm x).1 ≫ kerPairι G' φ = x.1.1
abbrev

kerPairιOver

L227 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairιOver
Documentation

The inclusion of the kernel intersection as a morphism over the base.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
abbrev kerPairιOver : SchemeHomOver (kerPairStr G' φ) f
theorem

kerPairPointEquiv_apply_coe

L230 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_apply_coe
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairPointEquiv_apply_coe {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (z : SchemeHomOver t (kerPairStr G' φ)) :
    (kerPairPointEquiv G' φ t z).1 = NeronModelInfra.schemeHomOverComp z (kerPairιOver G' φ)
theorem

kerPairPointEquiv_natural

L235 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_natural
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairPointEquiv_natural {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (t' : T' ⟶ Spec (CommRingCat.of R)) (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (z : SchemeHomOver t
      (kerPairStr G' φ)) :
    (kerPairPointEquiv G' φ t' (schemeHomOverComp ψ hψ z)).1 =
      schemeHomOverComp ψ hψ (kerPairPointEquiv G' φ t z).1
theorem

kerPairPoint_ext

L242 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPoint_ext
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPair
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem kerPairPoint_ext {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {z w : SchemeHomOver t
  (kerPairStr G' φ)}
    (h : z.1 ≫ kerPairι G' φ = w.1 ≫ kerPairι G' φ) : z = w
theorem

kerPair_mul_mem

L261 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPair_mul_mem
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
section
variable {G G' φ}
include hφ
Lean source · statement
theorem kerPair_mul_mem {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) {x y : SchemeHomOver t f}
    (hx : ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t)
    (hy : ∀ i, NeronModelInfra.schemeHomOverComp y (φ i) = G'.one t) (i : Fin 2) :
    NeronModelInfra.schemeHomOverComp (G.mul t x y) (φ i) = G'.one t
theorem

kerPair_one_mem

L267 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPair_one_mem
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
section
variable {G G' φ}
include hφ
Lean source · statement
theorem kerPair_one_mem {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (i : Fin 2) :
    NeronModelInfra.schemeHomOverComp (G.one t) (φ i) = G'.one t
theorem

kerPair_inv_mem

L271 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPair_inv_mem
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
section
variable {G G' φ}
include hφ
Lean source · statement
theorem kerPair_inv_mem {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) {x : SchemeHomOver t f}
    (hx : ∀ i, NeronModelInfra.schemeHomOverComp x (φ i) = G'.one t) (i : Fin 2) :
    NeronModelInfra.schemeHomOverComp (G.inv t x) (φ i) = G'.one t
def

kerPairLaw

L281 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairLaw
Documentation

The relative group law on the intersection of the kernels, transported from the source group.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · full declaration
def kerPairLaw : RelativeGroupLaw R (kerPairStr G' φ) where
  mul t z w := (kerPairPointEquiv G' φ t).symm
    ⟨G.mul t (kerPairPointEquiv G' φ t z).1 (kerPairPointEquiv G' φ t w).1,
      kerPair_mul_mem hφ t (kerPairPointEquiv G' φ t z).2 (kerPairPointEquiv G' φ t w).2⟩
  one t := (kerPairPointEquiv G' φ t).symm ⟨G.one t, kerPair_one_mem hφ t⟩
  inv t z := (kerPairPointEquiv G' φ t).symm
    ⟨G.inv t (kerPairPointEquiv G' φ t z).1, kerPair_inv_mem hφ t (kerPairPointEquiv G' φ t z).2⟩
  mul_assoc t x y z := by
    simp only [Equiv.apply_symm_apply, G.mul_assoc]
  one_mul t x := by
    simp only [Equiv.apply_symm_apply, G.one_mul, Subtype.coe_eta, Equiv.symm_apply_apply]
  mul_one t x := by
    simp only [Equiv.apply_symm_apply, G.mul_one, Subtype.coe_eta, Equiv.symm_apply_apply]
  inv_mul_cancel t x := by
    simp only [Equiv.apply_symm_apply, G.inv_mul_cancel]
  mul_natural t t' ψ hψ x y := by
    apply kerPairPoint_ext
    rw [schemeHomOverComp_coe, Category.assoc, kerPairPointEquiv_symm_apply_coe,
      kerPairPointEquiv_symm_apply_coe]
    have h := congrArg Subtype.val (G.mul_natural t t' ψ hψ (kerPairPointEquiv G' φ t x).1
      (kerPairPointEquiv G' φ t y).1)
    rw [schemeHomOverComp_coe] at h
    rw [h, ← kerPairPointEquiv_natural, ← kerPairPointEquiv_natural]
theorem

kerPairPointEquiv_mul

L305 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_mul
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem kerPairPointEquiv_mul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (z w : SchemeHomOver t (kerPairStr G' φ)) :
    (kerPairPointEquiv G' φ t ((kerPairLaw G G' φ hφ).mul t z w)).1 =
      G.mul t (kerPairPointEquiv G' φ t z).1 (kerPairPointEquiv G' φ t w).1
theorem

kerPairPointEquiv_one

L311 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_one
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem kerPairPointEquiv_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    (kerPairPointEquiv G' φ t ((kerPairLaw G G' φ hφ).one t)).1 = G.one t
theorem

kerPairPointEquiv_inv

L315 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_inv
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem kerPairPointEquiv_inv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (z : SchemeHomOver t (kerPairStr G' φ)) :
    (kerPairPointEquiv G' φ t ((kerPairLaw G G' φ hφ).inv t z)).1 =
      G.inv t (kerPairPointEquiv G' φ t z).1
theorem

kerPairι_isHom

L321 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairι_isHom
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem kerPairι_isHom : IsHom (kerPairLaw G G' φ hφ) G (kerPairιOver G' φ)
theorem

kerPairLaw

L326 ↗
GoodReductionJacobian.RelativeGroupLaw.IsCommutative.kerPairLaw
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem IsCommutative.kerPairLaw (hc : G.IsCommutative) : (kerPairLaw G G' φ hφ).IsCommutative
theorem

kerPairPointEquiv_nsmul

L332 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairPointEquiv_nsmul
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section KerPairLaw
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G : RelativeGroupLaw R f) (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
  (hφ : ∀ i, IsHom G G' (φ i))
Lean source · statement
theorem kerPairPointEquiv_nsmul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ)
    (z : SchemeHomOver t (kerPairStr G' φ)) :
    (kerPairPointEquiv G' φ t ((kerPairLaw G G' φ hφ).nsmul t n z)).1 = G.nsmul t n
      (kerPairPointEquiv G' φ t z).1
theorem

isClosedImmersion_one

L348 ↗
GoodReductionJacobian.RelativeGroupLaw.isClosedImmersion_one
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Properties
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
theorem isClosedImmersion_one [IsSeparated f'] :
    IsClosedImmersion (G'.one (𝟙 (Spec (CommRingCat.of R)))).1
instance

kerPairι_isClosedImmersion

L354 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairι_isClosedImmersion
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Properties
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
instance kerPairι_isClosedImmersion [IsSeparated f'] : IsClosedImmersion (kerPairι G' φ)
instance

kerPairStr_locallyOfFiniteType

L358 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairStr_locallyOfFiniteType
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Properties
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
instance kerPairStr_locallyOfFiniteType [IsSeparated f'] [LocallyOfFiniteType f] :
    LocallyOfFiniteType (kerPairStr G' φ)
instance

kerPairStr_quasiCompact

L362 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairStr_quasiCompact
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Properties
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
instance kerPairStr_quasiCompact [IsSeparated f'] [QuasiCompact f] : QuasiCompact (kerPairStr G' φ)
instance

kerPairStr_isSeparated

L366 ↗
GoodReductionJacobian.RelativeGroupLaw.kerPairStr_isSeparated
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Properties
variable {R : Type u} [CommRing R] {A A' : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec (CommRingCat.of R)}
variable (G' : RelativeGroupLaw R f') (φ : Fin 2 → SchemeHomOver f f')
Lean source · statement
instance kerPairStr_isSeparated [IsSeparated f'] [IsSeparated f] : IsSeparated (kerPairStr G' φ)

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