NYLL
Module

RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
30 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law exists smooth Of Relative Dimension of smooth of is Local Ring

Imports10
Imported by3

Declarations

theorem

appLE_basicOpen_basicOpen

L45 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.R1NeronObjE7.appLE_basicOpen_basicOpen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom
section descend
variable {P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
Lean source · statement
theorem appLE_basicOpen_basicOpen
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) (hPl : LocalizationAwayPreserves P)
    {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.affineOpens) (V : X.affineOpens)
    (e : V.1 ≤ f ⁻¹ᵁ U.1) (h : P (f.appLE U V e).hom)
    (r : Γ(Y, U)) (s : Γ(X, X.basicOpen (f.appLE U V e r)))
    (e' : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r) :
    P (f.appLE (Y.basicOpen r) (X.basicOpen s) e').hom
theorem

eq_of_isStandardSmoothOfRelativeDimension_appLE

L69 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.R1NeronObjE7.eq_of_isStandardSmoothOfRelativeDimension_appLE
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom
Lean source · statement
theorem eq_of_isStandardSmoothOfRelativeDimension_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    {n n' : ℕ}
    (U : Y.affineOpens) (V : X.affineOpens) (hx : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1)
    (h : (f.appLE U V e).hom.IsStandardSmoothOfRelativeDimension n)
    (U' : Y.affineOpens) (V' : X.affineOpens) (hx' : x ∈ V'.1) (e' : V'.1 ≤ f ⁻¹ᵁ U'.1)
    (h' : (f.appLE U' V' e').hom.IsStandardSmoothOfRelativeDimension n') : n = n'
theorem

exists_chart

L113 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.R1NeronObjE7.exists_chart
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom
Lean source · statement
theorem exists_chart {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] (x : X) :
    ∃ (n : ℕ) (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1),
      (f.appLE U V e).hom.IsStandardSmoothOfRelativeDimension n
def

HasChart

L131 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.HasChart
Documentation

An affine chart around a point on which the structure map is standard smooth of dimension n.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
def HasChart {X Y : Scheme.{u}} (n : ℕ) (f : X ⟶ Y) (x : X) : Prop
theorem

unique

L135 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.HasChart.unique
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem HasChart.unique {X Y : Scheme.{u}} {n m : ℕ} {f : X ⟶ Y} {x : X}
    (h : HasChart n f x) (h' : HasChart m f x) : n = m
theorem

of_smoothOfRelativeDimension

L141 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.HasChart.of_smoothOfRelativeDimension
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem HasChart.of_smoothOfRelativeDimension {X Y : Scheme.{u}} (n : ℕ) (f : X ⟶ Y)
    [SmoothOfRelativeDimension n f] (x : X) : HasChart n f x
theorem

exists_hasChart

L147 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.exists_hasChart
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem exists_hasChart {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] (x : X) : ∃ n, HasChart n f x
theorem

of_comp_isOpenImmersion

L152 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.HasChart.of_comp_isOpenImmersion
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem HasChart.of_comp_isOpenImmersion {W X Y : Scheme.{u}} {n : ℕ} (j : W ⟶ X) [IsOpenImmersion
  j]
    (g : X ⟶ Y) {w : W} (h : HasChart n (j ≫ g) w) : HasChart n g (j.base w)
theorem

snd

L168 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.HasChart.snd
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem HasChart.snd {X : Scheme.{u}} {S : Scheme.{u}} {n : ℕ} (f : X ⟶ S)
    {w : ↑(pullback f f)} (h : HasChart n f ((pullback.fst f f).base w)) :
    HasChart n (pullback.snd f f) w
abbrev

tt

L220 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.tt
Documentation

The common structure map of the product of the relative group with itself.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
abbrev tt (f : X ⟶ Spec (CommRingCat.of R)) : pullback f f ⟶ Spec (CommRingCat.of R)
def

pa

L224 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.pa
Documentation

The first projection, regarded as a point of the relative group over the product.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
def pa (f : X ⟶ Spec (CommRingCat.of R)) : SchemeHomOver (tt f) f
def

pb

L226 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.pb
Documentation

The second projection, regarded as a point of the relative group over the product.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
def pb (f : X ⟶ Spec (CommRingCat.of R)) : SchemeHomOver (tt f) f
theorem

inv_natural

L229 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.inv_natural
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem inv_natural {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (t' : T' ⟶ Spec
  (CommRingCat.of R))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) :
    schemeHomOverComp ψ hψ (G.inv t x) = G.inv t' (schemeHomOverComp ψ hψ x)
def

sigmaHom

L242 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaHom
Documentation

Translation on the product that sends (a, b) to (a * b⁻¹, b).

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
def sigmaHom : pullback f f ⟶ pullback f f
def

sigmaInv

L247 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaInv
Documentation

The inverse translation on the product that sends (a, b) to (a * b, b).

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
def sigmaInv : pullback f f ⟶ pullback f f
theorem

sigmaHom_tt

L251 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaHom_tt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem sigmaHom_tt : sigmaHom G ≫ tt f = tt f
theorem

sigmaInv_tt

L256 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaInv_tt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem sigmaInv_tt : sigmaInv G ≫ tt f = tt f
theorem

comp_sigmaHom_pa

L261 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.comp_sigmaHom_pa
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem comp_sigmaHom_pa : schemeHomOverComp (sigmaHom G) (sigmaHom_tt G) (pa f) =
    G.mul (tt f) (pa f) (G.inv (tt f) (pb f))
theorem

comp_sigmaHom_pb

L265 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.comp_sigmaHom_pb
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem comp_sigmaHom_pb : schemeHomOverComp (sigmaHom G) (sigmaHom_tt G) (pb f) = pb f
theorem

comp_sigmaInv_pa

L268 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.comp_sigmaInv_pa
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem comp_sigmaInv_pa : schemeHomOverComp (sigmaInv G) (sigmaInv_tt G) (pa f) =
    G.mul (tt f) (pa f) (pb f)
theorem

comp_sigmaInv_pb

L272 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.comp_sigmaInv_pb
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem comp_sigmaInv_pb : schemeHomOverComp (sigmaInv G) (sigmaInv_tt G) (pb f) = pb f
theorem

sigmaHom_sigmaInv

L275 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaHom_sigmaInv
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem sigmaHom_sigmaInv : sigmaHom G ≫ sigmaInv G = 𝟙 _
theorem

sigmaInv_sigmaHom

L285 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigmaInv_sigmaHom
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem sigmaInv_sigmaHom : sigmaInv G ≫ sigmaHom G = 𝟙 _
def

sigma

L297 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigma
Documentation

The translation isomorphism of the product obtained from multiplication and inversion.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · full declaration
def sigma : pullback f f ≅ pullback f f where
  hom := sigmaHom G
  inv := sigmaInv G
  hom_inv_id := sigmaHom_sigmaInv G
  inv_hom_id := sigmaInv_sigmaHom G
theorem

sigma_inv_snd

L303 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.sigma_inv_snd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem sigma_inv_snd : (sigma G).inv ≫ pullback.snd f f = pullback.snd f f
def

delta

L307 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.delta
Documentation

The diagonal map of the relative group into its product over the base.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
def delta (f : X ⟶ Spec (CommRingCat.of R)) : X ⟶ pullback f f
theorem

delta_tt

L309 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.delta_tt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem delta_tt : delta f ≫ tt f = f
theorem

delta_sigmaHom_fst

L313 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.delta_sigmaHom_fst
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
section Translation
variable {R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f)
Lean source · statement
theorem delta_sigmaHom_fst : delta f ≫ sigmaHom G ≫ pullback.fst f f = f ≫ (G.one (𝟙 _)).1
theorem

main

L329 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing.P2mSmoothDim.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
noncomputable section
namespace P2mSmoothDim
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits RingHom
Lean source · statement
theorem main {R : Type u} [CommRing R] [IsLocalRing R] {X : Scheme.{u}} {f : X ⟶ Spec
  (CommRingCat.of R)}
    [Smooth f] (G : RelativeGroupLaw R f) : ∃ d : ℕ, SmoothOfRelativeDimension d f
theorem

exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing

L379 ↗
GoodReductionJacobian.RelativeGroupLaw.exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
Source context 6 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian in
Lean source · statement
theorem exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing
    {R : Type u} [CommRing R] [IsLocalRing R] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of R)}
      [Smooth f]
    (G : RelativeGroupLaw R f) :
    ∃ d : ℕ, SmoothOfRelativeDimension d f

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