Module

Translation.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Translation

20 declarations indexed from sourceView source ↗

Module documentation

Translation

Imports4

Mathlib.AlgebraicGeometry.Modules.Sheaf
Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Kernel
Nyll.AlgebraicCurves.Geometry.Picard.Functor

Imported by10

def

LocallyIsoOver

L34 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver

Documentation

Two modules are locally isomorphic on inverse images of open neighborhoods in the base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}

Lean source · statement

def LocallyIsoOver (q : X ⟶ T) (M M' : X.Modules) : Prop

theorem

of_iso

L43 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver.of_iso

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 AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}
namespace LocallyIsoOver
variable {q : X ⟶ T} {M M' M'' : X.Modules}

Lean source · statement

theorem of_iso (q : X ⟶ T) {M M' : X.Modules} (e : M ≅ M') : LocallyIsoOver q M M'

theorem

rfl

L46 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver.rfl

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 AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}
namespace LocallyIsoOver
variable {q : X ⟶ T} {M M' M'' : X.Modules}

Lean source · statement

theorem rfl : LocallyIsoOver q M M

theorem

symm

L48 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver.symm

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 AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}
namespace LocallyIsoOver
variable {q : X ⟶ T} {M M' M'' : X.Modules}

Lean source · statement

theorem symm (h : LocallyIsoOver q M M') : LocallyIsoOver q M' M

def

restrict

L53 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver.restrict

Documentation

The restriction of a module isomorphism to the inverse image of a smaller open.

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 AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}
namespace LocallyIsoOver
variable {q : X ⟶ T} {M M' M'' : X.Modules}

Lean source · statement

def restrict {U V : T.Opens} (hVU : V ≤ U)
    (e : (Scheme.Modules.pullback (q ⁻¹ᵁ U).ι).obj M ≅ (Scheme.Modules.pullback (q ⁻¹ᵁ U).ι).obj
      M') :
    (Scheme.Modules.pullback (q ⁻¹ᵁ V).ι).obj M ≅ (Scheme.Modules.pullback (q ⁻¹ᵁ V).ι).obj M'

theorem

trans

L64 ↗

AlgebraicGeometry.Scheme.Modules.LocallyIsoOver.trans

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 AlgebraicGeometry.Scheme.Modules
variable {X T : Scheme.{u}}
namespace LocallyIsoOver
variable {q : X ⟶ T} {M M' M'' : X.Modules}

Lean source · statement

theorem trans (h : LocallyIsoOver q M M') (h' : LocallyIsoOver q M' M'') : LocallyIsoOver q M M''

def

fstPoint

L79 ↗

GoodReductionJacobian.RelativeGroupLaw.fstPoint

Documentation

The point of the original group scheme given by the first base-change projection.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def fstPoint (_L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    SchemeHomOver (pullback.snd f t ≫ t) f

def

sndPoint

L84 ↗

GoodReductionJacobian.RelativeGroupLaw.sndPoint

Documentation

The chosen point transported along the second base-change projection.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def sndPoint (_L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (x : SchemeHomOver t f) : SchemeHomOver (pullback.snd f t ≫ t) f

theorem

fstPoint_coe

L88 ↗

GoodReductionJacobian.RelativeGroupLaw.fstPoint_coe

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem fstPoint_coe (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R)) :
    (L.fstPoint t).1 = pullback.fst f t

theorem

sndPoint_coe

L92 ↗

GoodReductionJacobian.RelativeGroupLaw.sndPoint_coe

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem sndPoint_coe (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
    (x : SchemeHomOver t f) : (L.sndPoint t x).1 = pullback.snd f t ≫ x.1

def

mulRight

L97 ↗

GoodReductionJacobian.RelativeGroupLaw.mulRight

Documentation

The morphism given by right multiplication by the chosen point after base change.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def mulRight (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (x : SchemeHomOver t f) : pullback f t ⟶ A

theorem

mulRight_over

L101 ↗

GoodReductionJacobian.RelativeGroupLaw.mulRight_over

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem mulRight_over (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (x : SchemeHomOver t f) : L.mulRight t x ≫ f = pullback.snd f t ≫ t

theorem

sndPoint_one

L105 ↗

GoodReductionJacobian.RelativeGroupLaw.sndPoint_one

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem sndPoint_one (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    L.sndPoint t (L.one t) = L.one (pullback.snd f t ≫ t)

theorem

mulRight_one

L111 ↗

GoodReductionJacobian.RelativeGroupLaw.mulRight_one

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem mulRight_one (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    L.mulRight t (L.one t) = pullback.fst f t

def

translate

L118 ↗

GoodReductionJacobian.RelativeGroupLaw.translate

Documentation

The translation morphism given by right multiplication by a section over the base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def translate (L : RelativeGroupLaw R f) (x : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) f) : A ⟶
  A

theorem

translate_over

L122 ↗

GoodReductionJacobian.RelativeGroupLaw.translate_over

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem translate_over (L : RelativeGroupLaw R f) (x : SchemeHomOver (𝟙 (Spec (CommRingCat.of R)))
  f) :
    L.translate x ≫ f = f

theorem

translate_one

L127 ↗

GoodReductionJacobian.RelativeGroupLaw.translate_one

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem translate_one (L : RelativeGroupLaw R f) : L.translate (L.one (𝟙 (Spec (CommRingCat.of
  R)))) = 𝟙 A

def

IsInStabilizer

L140 ↗

GoodReductionJacobian.RelativeGroupLaw.IsInStabilizer

Documentation

Translation by the point preserves the module up to isomorphism locally on the base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def IsInStabilizer (L : RelativeGroupLaw R f) (𝓛 : A.Modules) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
    (x : SchemeHomOver t f) : Prop

theorem

isInStabilizer_one

L147 ↗

GoodReductionJacobian.RelativeGroupLaw.isInStabilizer_one

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem isInStabilizer_one (L : RelativeGroupLaw R f) (𝓛 : A.Modules) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) : L.IsInStabilizer 𝓛 t (L.one t)

theorem

isInStabilizer_unit

L153 ↗

GoodReductionJacobian.RelativeGroupLaw.isInStabilizer_unit

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem isInStabilizer_unit (L : RelativeGroupLaw R f) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
    (x : SchemeHomOver t f) : L.IsInStabilizer (SheafOfModules.unit A.ringCatSheaf) t x

Module documentation

Translation

Declarations