NYLL
Module

RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
40 declarations indexed from sourceView source ↗

Module documentation

Etaleness of an endomorphism kernel

The action on the maximal ideal controls infinitesimal points of a polynomial endomorphism.

Imports9
Imported by1

Declarations

theorem

formallyUnramified_of_forall_derivation_eq_zero

L46 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.formallyUnramified_of_forall_derivation_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Algebra
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
Lean source · statement
theorem formallyUnramified_of_forall_derivation_eq_zero [Algebra.EssFiniteType R S]
    (H : ∀ (m : Ideal S) (_ : m.IsMaximal) (δ : Derivation R S (S ⧸ m)), δ = 0) :
    Algebra.FormallyUnramified R S
def

π₀

L82 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.π₀
Documentation

Projection from the dual numbers to their constant coefficient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def π₀ : DualNumber K →+* K
def

ι₀

L85 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ι₀
Documentation

The inclusion of constants into the dual numbers.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def ι₀ : K →+* DualNumber K
def

g₀

L88 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.g₀
Documentation

The endomorphism of dual numbers discarding the infinitesimal part.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def g₀ : DualNumber K →+* DualNumber K
theorem

π₀_apply

L90 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.π₀_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem π₀_apply (z : DualNumber K) : π₀ K z = z.fst
theorem

ι₀_apply

L92 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ι₀_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem ι₀_apply (c : K) : ι₀ K c = TrivSqZeroExt.inl c
theorem

g₀_apply

L94 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.g₀_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem g₀_apply (z : DualNumber K) : g₀ K z = TrivSqZeroExt.inl z.fst
theorem

g₀_eq_self_iff

L96 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.g₀_eq_self_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem g₀_eq_self_iff (z : DualNumber K) : g₀ K z = z ↔ z.snd = 0
theorem

π₀_comp_ι₀

L102 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.π₀_comp_ι₀
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem π₀_comp_ι₀ : (π₀ K).comp (ι₀ K) = RingHom.id K
theorem

π₀_surjective

L105 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.π₀_surjective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem π₀_surjective : Function.Surjective (π₀ K)
abbrev

SK

L108 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.SK
Documentation

The spectrum of the base field.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
abbrev SK : Scheme.{u}
abbrev

SKε

L111 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.SKε
Documentation

The spectrum of the dual numbers.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
abbrev SKε : Scheme.{u}
def

pε

L114 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.pε
Documentation

The structure map of the dual-number point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def pε : SKε K ⟶ SK K
def

iε

L117 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.iε
Documentation

The zero section of the dual-number point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def iε : SK K ⟶ SKε K
def

ρ

L120 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ρ
Documentation

The endomorphism projecting an infinitesimal point to its constant part.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
def ρ : SKε K ⟶ SKε K
theorem

ρ_eq

L122 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ρ_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem ρ_eq : ρ K = pε K ≫ iε K
theorem

iε_comp_pε

L125 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.iε_comp_pε
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem iε_comp_pε : iε K ≫ pε K = 𝟙 _
theorem

iε_comp_ρ

L129 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.iε_comp_ρ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem iε_comp_ρ : iε K ≫ ρ K = iε K
theorem

ρ_comp_pε

L132 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ρ_comp_pε
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem ρ_comp_pε : ρ K ≫ pε K = pε K
instance

(anonymous instance)

L135 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
instance : IsClosedImmersion (iε K)
theorem

isNilpotent_ker_specMap

L138 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.isNilpotent_ker_specMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem isNilpotent_ker_specMap {R' S' : CommRingCat.{u}} (φ : R' ⟶ S')
    (h2 : ∀ a ∈ RingHom.ker φ.hom, ∀ b ∈ RingHom.ker φ.hom, a * b = 0) :
    IsNilpotent (Spec.map φ).ker
theorem

isNilpotent_ker_iε

L164 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.isNilpotent_ker_iε
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem isNilpotent_ker_iε : IsNilpotent (iε K).ker
theorem

not_isUnit_iff_fst_eq_zero

L172 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.not_isUnit_iff_fst_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Dual
variable (K : Type u) [Field K]
Lean source · statement
theorem not_isUnit_iff_fst_eq_zero (z : DualNumber K) : ¬ IsUnit z ↔ z.fst = 0
def

κ

L182 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.κ
Documentation

A base-field element represented in the stalk at a point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Tangent
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
def κ (y : A) (c : K) : A.presheaf.stalk y
theorem

stalkMap_κ

L185 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.stalkMap_κ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Tangent
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem stalkMap_κ (π : SchemeHomOver f f) (x : A) (c : K) :
    π.1.stalkMap x (κ f (π.1.base x) c) = κ f x c
theorem

stalkClosedPointTo_κ

L197 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.stalkClosedPointTo_κ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Tangent
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem stalkClosedPointTo_κ (w : SKε K ⟶ A) (hw : w ≫ f = pε K) (c : K) :
    Scheme.stalkClosedPointTo w (κ f (w.base (IsLocalRing.closedPoint (DualNumber K))) c) = ι₀ K c
theorem

stalk_ktv

L214 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.stalk_ktv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Tangent
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem stalk_ktv (π : SchemeHomOver f f)
    (hdπ : ∀ x : A, (IsLocalRing.maximalIdeal (A.presheaf.stalk (π.1.base x))).map (π.1.stalkMap
      x).hom ≤
      IsLocalRing.maximalIdeal (A.presheaf.stalk x) ^ 2)
    (w : SKε K ⟶ A) (hw : w ≫ f = pε K) :
    π.1.stalkMap (w.base (IsLocalRing.closedPoint (DualNumber K))) ≫ Scheme.stalkClosedPointTo w =
      (π.1.stalkMap (w.base (IsLocalRing.closedPoint (DualNumber K))) ≫ Scheme.stalkClosedPointTo
        w) ≫
        CommRingCat.ofHom (g₀ K)
theorem

comp_ktv

L272 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.comp_ktv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Tangent
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem comp_ktv (π : SchemeHomOver f f)
    (hdπ : ∀ x : A, (IsLocalRing.maximalIdeal (A.presheaf.stalk (π.1.base x))).map (π.1.stalkMap
      x).hom ≤
      IsLocalRing.maximalIdeal (A.presheaf.stalk x) ^ 2)
    (w : SKε K ⟶ A) (hw : w ≫ f = pε K) :
    ρ K ≫ w ≫ π.1 = w ≫ π.1
def

fixSub

L297 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.fixSub
Documentation

The subgroup fixed by a group endomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Group
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · full declaration
def fixSub {M : Type*} [Group M] (F : M →* M) : Subgroup M where
  carrier := {u | F u = u}
  mul_mem' := by
    intro a b ha hb
    simp only [Set.mem_ofPred_eq] at ha hb ⊢
    rw [map_mul, ha, hb]
  one_mem' := map_one F
  inv_mem' := by
    intro a ha
    simp only [Set.mem_ofPred_eq] at ha ⊢
    rw [map_inv, ha]
def

pullHom

L310 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.pullHom
Documentation

Pullback of points as a group homomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Group
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · full declaration
def pullHom (L : RelativeGroupLaw K f) (hc : L.IsCommutative) {T T' : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of K)} {t' : T' ⟶ Spec (CommRingCat.of K)} (ψ : T' ⟶ T)
    (hψ : ψ ≫ t = t') :
    letI := L.pointCommGroup hc t
    letI := L.pointCommGroup hc t'
    SchemeHomOver t f →* SchemeHomOver t' f :=
  letI := L.pointCommGroup hc t
  letI := L.pointCommGroup hc t'
  { toFun := GoodReductionJacobian.schemeHomOverComp ψ hψ
    map_one' := L.one_natural t t' ψ hψ
    map_mul' := L.mul_natural t t' ψ hψ }
theorem

pullHom_apply_coe

L322 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.pullHom_apply_coe
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Group
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem pullHom_apply_coe (L : RelativeGroupLaw K f) (hc : L.IsCommutative) {T T' : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of K)} {t' : T' ⟶ Spec (CommRingCat.of K)} (ψ : T' ⟶ T)
    (hψ : ψ ≫ t = t') (φ : SchemeHomOver t f) :
    (pullHom L hc ψ hψ φ).1 = ψ ≫ φ.1
theorem

pow_eq_nsmul

L327 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.pow_eq_nsmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Group
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · full declaration
theorem pow_eq_nsmul (L : RelativeGroupLaw K f) (hc : L.IsCommutative) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (x : SchemeHomOver t f) (n : ℕ) :
    (letI := L.pointCommGroup hc t; x ^ n) = L.nsmul t n x := by
  let := L.pointCommGroup hc t
  induction n with
  | zero => rfl
  | succ n ih => rw [pow_succ, ih]; rfl
theorem

ρ_comp_eq_of_endAeval

L335 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ρ_comp_eq_of_endAeval
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Group
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem ρ_comp_eq_of_endAeval (L : RelativeGroupLaw K f) (hc : L.IsCommutative) (π : SchemeHomOver
  f f)
    (hπ : ∀ w : SchemeHomOver (pε K) f, ρ K ≫ w.1 ≫ π.1 = w.1 ≫ π.1)
    (G : Polynomial ℤ) (hG : ((G.coeff 0 : ℤ) : K) ≠ 0) (v : SchemeHomOver (pε K) f)
    (hv : ρ K ≫ v.1 ≫ (L.endAeval hc π G).1 = v.1 ≫ (L.endAeval hc π G).1) :
    ρ K ≫ v.1 = v.1
theorem

appLE_congrHom

L410 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.appLE_congrHom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem appLE_congrHom {X Y : Scheme.{u}} {g g' : X ⟶ Y} (h : g = g') (U : Y.Opens) (V : X.Opens)
    (e : V ≤ g ⁻¹ᵁ U) (e' : V ≤ g' ⁻¹ᵁ U) : g.appLE U V e = g'.appLE U V e'
def

ιop

L415 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ιop
Documentation

The base-field map to sections over an open subset.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
def ιop (V : A.Opens) : CommRingCat.of K ⟶ Γ(A, V)
theorem

fromSpec_comp_eq

L419 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.fromSpec_comp_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem fromSpec_comp_eq (V : A.Opens) (hV : IsAffineOpen V) :
    hV.fromSpec ≫ f = Spec.map (ιop f V)
theorem

ιop_finiteType

L426 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ιop_finiteType
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem ιop_finiteType [LocallyOfFiniteType f] (V : A.Opens) (hV : IsAffineOpen V) :
    (ιop f V).hom.FiniteType
theorem

ιop_comp_appLE

L434 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.ιop_comp_appLE
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem ιop_comp_appLE (β : SchemeHomOver f f) (U V : A.Opens) (hVU : V ≤ β.1 ⁻¹ᵁ U) :
    ιop f U ≫ β.1.appLE U V hVU = ιop f V
theorem

formallyUnramified_endAeval

L440 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep.formallyUnramified_endAeval
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mFrobSep
section Assembly
variable {K : Type u} [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
Lean source · statement
theorem formallyUnramified_endAeval [IsAlgClosed K] [LocallyOfFiniteType f]
    (L : RelativeGroupLaw K f) (hc : L.IsCommutative) (π : SchemeHomOver f f)
    (hdπ : ∀ x : A, (IsLocalRing.maximalIdeal (A.presheaf.stalk (π.1.base x))).map (π.1.stalkMap
      x).hom ≤
      IsLocalRing.maximalIdeal (A.presheaf.stalk x) ^ 2)
    (G : Polynomial ℤ) (hG : ((G.coeff 0 : ℤ) : K) ≠ 0) :
    FormallyUnramified (L.endAeval hc π G).1
theorem

etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq

L570 ↗
GoodReductionJacobian.RelativeGroupLaw.etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
Source context 6 commands

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

section ProofImplementation
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq.P2mFrobSep
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry GoodReductionJacobian NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
universe u
Lean source · statement
theorem etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq
    (K : Type u) [Field K] [IsAlgClosed K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
    (L : RelativeGroupLaw K f) (hc : L.IsCommutative) (hA : AbelianSchemePropertyBundle K f)
    (π : SchemeHomOver f f)
    (hdπ : ∀ x : A, (IsLocalRing.maximalIdeal (A.presheaf.stalk (π.1.base x))).map (π.1.stalkMap
      x).hom ≤
      IsLocalRing.maximalIdeal (A.presheaf.stalk x) ^ 2)
    (G : Polynomial ℤ) (hG : ((G.coeff 0 : ℤ) : K) ≠ 0) :
    Etale (L.endKerStr (L.endAeval hc π G))

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