NYLL
Module

Fibre.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Fibre
18 declarations indexed from sourceView source ↗

Module documentation

Fibre

Imports4
Imported by9

Declarations

abbrev

baseResidueField

L34 ↗
GoodReductionJacobian.RelativeGroupLaw.baseResidueField
Documentation

The residue field of a point of the base spectrum.

Source context 6 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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev baseResidueField (s : (Spec (CommRingCat.of R) : Scheme.{u})) : Type u
abbrev

basePointInclusion

L38 ↗
GoodReductionJacobian.RelativeGroupLaw.basePointInclusion
Documentation

The canonical morphism from the spectrum of the residue field to the base.

Source context 6 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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev basePointInclusion (s : (Spec (CommRingCat.of R) : Scheme.{u})) :
    Spec (CommRingCat.of (baseResidueField s)) ⟶ Spec (CommRingCat.of R)
abbrev

fibreScheme

L43 ↗
GoodReductionJacobian.RelativeGroupLaw.fibreScheme
Documentation

The scheme-theoretic fibre over the specified point of the base.

Source context 6 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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev fibreScheme (f : A ⟶ Spec (CommRingCat.of R)) (s : (Spec (CommRingCat.of R) : Scheme.{u})) :
    Scheme.{u}
abbrev

fibreStr

L48 ↗
GoodReductionJacobian.RelativeGroupLaw.fibreStr
Documentation

The structure morphism of the fibre over its residue field.

Source context 6 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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev fibreStr (f : A ⟶ Spec (CommRingCat.of R)) (s : (Spec (CommRingCat.of R) : Scheme.{u})) :
    fibreScheme f s ⟶ Spec (CommRingCat.of (baseResidueField s))
theorem

fibreScheme_eq_fiber

L54 ↗
GoodReductionJacobian.RelativeGroupLaw.fibreScheme_eq_fiber
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibreScheme_eq_fiber : fibreScheme f s = f.fiber s
theorem

fibreStr_eq_fiberToSpecResidueField

L56 ↗
GoodReductionJacobian.RelativeGroupLaw.fibreStr_eq_fiberToSpecResidueField
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibreStr_eq_fiberToSpecResidueField :
    fibreStr f s = f.fiberToSpecResidueField s
def

fibrePointToBase

L60 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase
Documentation

A point of the fibre viewed as a point of the original scheme over the base.

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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
def fibrePointToBase {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))}
    (x : SchemeHomOver t' (fibreStr f s)) : SchemeHomOver (t' ≫ basePointInclusion s) f
def

fibrePointOfBase

L66 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase
Documentation

A point over the residue field lifted to the fibre by the pullback property.

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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
def fibrePointOfBase {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))}
    (y : SchemeHomOver (t' ≫ basePointInclusion s) f) : SchemeHomOver t' (fibreStr f s)
theorem

fibrePointToBase_coe

L70 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_coe
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibrePointToBase_coe {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))}
    (x : SchemeHomOver t' (fibreStr f s)) :
    (fibrePointToBase s x).1 = x.1 ≫ pullback.fst f (basePointInclusion s)
theorem

fibrePointOfBase_coe

L75 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_coe
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibrePointOfBase_coe {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))}
    (y : SchemeHomOver (t' ≫ basePointInclusion s) f) :
    (fibrePointOfBase s y).1 = pullback.lift y.1 t' y.2
theorem

fibrePointToBase_ofBase

L80 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_ofBase
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibrePointToBase_ofBase {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField
  s))}
    (y : SchemeHomOver (t' ≫ basePointInclusion s) f) :
    fibrePointToBase s (fibrePointOfBase s y) = y
theorem

fibrePointOfBase_toBase

L86 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_toBase
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibrePointOfBase_toBase {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of (baseResidueField
  s))}
    (x : SchemeHomOver t' (fibreStr f s)) :
    fibrePointOfBase s (fibrePointToBase s x) = x
def

fibrePointEquiv

L97 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointEquiv
Documentation

The equivalence between fibre-valued points and compatible points of the original 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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · full declaration
def fibrePointEquiv {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))) :
    SchemeHomOver t' (fibreStr f s) ≃ SchemeHomOver (t' ≫ basePointInclusion s) f where
  toFun := fibrePointToBase s
  invFun := fibrePointOfBase s
  left_inv := fibrePointOfBase_toBase s
  right_inv := fibrePointToBase_ofBase s
theorem

fibrePointToBase_schemeHomOverComp

L104 ↗
GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_schemeHomOverComp
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · full declaration
theorem fibrePointToBase_schemeHomOverComp {T T' : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of (baseResidueField s)))
    (t' : T' ⟶ Spec (CommRingCat.of (baseResidueField s))) (ψ : T' ⟶ T) (hψ : ψ ≫ t = t')
    (x : SchemeHomOver t (fibreStr f s)) :
    fibrePointToBase s (schemeHomOverComp ψ hψ x) =
      schemeHomOverComp ψ (by rw [← Category.assoc, hψ]) (fibrePointToBase s x) :=
  Subtype.ext (Category.assoc _ _ _)
def

fibre

L113 ↗
GoodReductionJacobian.RelativeGroupLaw.fibre
Documentation

The relative group law induced on the scheme-theoretic fibre.

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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · full declaration
def fibre (G : RelativeGroupLaw R f) : RelativeGroupLaw (baseResidueField s) (fibreStr f s) where
  mul t' x y := fibrePointOfBase s (G.mul _ (fibrePointToBase s x) (fibrePointToBase s y))
  one t' := fibrePointOfBase s (G.one _)
  inv t' x := fibrePointOfBase s (G.inv _ (fibrePointToBase s x))
  mul_assoc t' x y z := by
    simp only [fibrePointToBase_ofBase, G.mul_assoc]
  one_mul t' x := by
    simp only [fibrePointToBase_ofBase, G.one_mul, fibrePointOfBase_toBase]
  mul_one t' x := by
    simp only [fibrePointToBase_ofBase, G.mul_one, fibrePointOfBase_toBase]
  inv_mul_cancel t' x := by
    simp only [fibrePointToBase_ofBase, G.inv_mul_cancel]
  mul_natural t t' ψ hψ x y := by
    apply Subtype.ext
    apply pullback.hom_ext
    · rw [schemeHomOverComp_coe, fibrePointOfBase_coe, fibrePointOfBase_coe, Category.assoc,
        pullback.lift_fst,
        pullback.lift_fst]
      have h := congrArg Subtype.val
        (G.mul_natural (t ≫ basePointInclusion s) (t' ≫ basePointInclusion s) ψ
          (by rw [← Category.assoc, hψ]) (fibrePointToBase s x) (fibrePointToBase s y))
      rw [schemeHomOverComp_coe] at h
      rw [h, ← fibrePointToBase_schemeHomOverComp, ← fibrePointToBase_schemeHomOverComp]
    · rw [schemeHomOverComp_coe, fibrePointOfBase_coe, fibrePointOfBase_coe, Category.assoc,
        pullback.lift_snd,
        pullback.lift_snd]
      exact hψ
theorem

fibre_mul

L141 ↗
GoodReductionJacobian.RelativeGroupLaw.fibre_mul
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibre_mul (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))) (x y : SchemeHomOver t' (fibreStr f s)) :
    (G.fibre s).mul t' x y = fibrePointOfBase s (G.mul _ (fibrePointToBase s x) (fibrePointToBase s
      y))
theorem

fibre_one

L147 ↗
GoodReductionJacobian.RelativeGroupLaw.fibre_one
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibre_one (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))) :
    (G.fibre s).one t' = fibrePointOfBase s (G.one _)
theorem

fibre_inv

L152 ↗
GoodReductionJacobian.RelativeGroupLaw.fibre_inv
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
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
variable (s : (Spec (CommRingCat.of R) : Scheme.{u}))
Lean source · statement
theorem fibre_inv (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t' : T ⟶ Spec (CommRingCat.of (baseResidueField s))) (x : SchemeHomOver t' (fibreStr f s)) :
    (G.fibre s).inv t' x = fibrePointOfBase s (G.inv _ (fibrePointToBase s x))

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