Module

RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat

5 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law end Degree scheme Hom Over Comp of is Finite of flat

Imports5

Imported by2

theorem

endDegree_eq_finrank_unit

L38 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat.P2mDegMul.endDegree_eq_finrank_unit

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mDegMul
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem endDegree_eq_finrank_unit (L : RelativeGroupLaw K f) (β : SchemeHomOver f f)
    [IsFinite β.1] [Flat β.1] :
    L.endDegree β =
      β.1.finrank ((L.one (𝟙 (Spec (CommRingCat.of K)))).1 (IsLocalRing.closedPoint K))

theorem

finrank_eq_finrank

L46 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat.P2mDegMul.finrank_eq_finrank

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mDegMul
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem finrank_eq_finrank [LocallyOfFiniteType f] (β : SchemeHomOver f f) [IsFinite β.1]
    [Flat β.1] [PreconnectedSpace A] (x y : A) : β.1.finrank x = β.1.finrank y

theorem

endDegree_eq_finrank

L53 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat.P2mDegMul.endDegree_eq_finrank

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mDegMul
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem endDegree_eq_finrank [LocallyOfFiniteType f] (L : RelativeGroupLaw K f)
    (β : SchemeHomOver f f) [IsFinite β.1] [Flat β.1] [PreconnectedSpace A] (x : A) :
    L.endDegree β = β.1.finrank x

theorem

main

L59 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat.P2mDegMul.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_endDegree_schemeHomOverComp_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mDegMul
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem main [LocallyOfFiniteType f] [PreconnectedSpace A] (L : RelativeGroupLaw K f)
    (β γ : SchemeHomOver f f) [IsFinite β.1] [Flat β.1] [IsFinite γ.1] [Flat γ.1] :
    L.endDegree (NeronModelInfra.schemeHomOverComp β γ) = L.endDegree β * L.endDegree γ

theorem

endDegree_schemeHomOverComp_of_isFinite_of_flat

L75 ↗

GoodReductionJacobian.RelativeGroupLaw.endDegree_schemeHomOverComp_of_isFinite_of_flat

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_endDegree_schemeHomOverComp_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u

Lean source · statement

theorem
  _root_.GoodReductionJacobian.RelativeGroupLaw.endDegree_schemeHomOverComp_of_isFinite_of_flat
    (K : Type u) [Field K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType
      f]
    [PreconnectedSpace A] (L : RelativeGroupLaw K f) (β γ : SchemeHomOver f f)
    [IsFinite β.1] [Flat β.1] [IsFinite γ.1] [Flat γ.1] :
    L.endDegree (NeronModelInfra.schemeHomOverComp β γ) = L.endDegree β * L.endDegree γ

Module documentation

Relative Group Law end Degree scheme Hom Over Comp of is Finite of flat

Declarations

endDegree_eq_finrank_unit

finrank_eq_finrank

endDegree_eq_finrank

main

endDegree_schemeHomOverComp_of_isFinite_of_flat