Module

RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat

7 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law surjective and end Degree eq finrank of is Finite of flat

Imports4

Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.EndDegree
Mathlib.AlgebraicGeometry.Noetherian

Imported by3

theorem

endDegree_eq_finrank_unit

L37 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat.P2mKerRank.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_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKerRank
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

L45 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat.P2mKerRank.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_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKerRank
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_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat.P2mKerRank.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_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKerRank
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

one_le_finrank

L59 ↗

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

Lean source · statement

theorem one_le_finrank [LocallyOfFiniteType f] (β : SchemeHomOver f f) [IsFinite β.1] [Flat β.1]
    [PreconnectedSpace A] (x : A) : 1 ≤ β.1.finrank x

theorem

surjective

L64 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat.P2mKerRank.surjective

Source context 8 commands

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

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

Lean source · statement

theorem surjective [LocallyOfFiniteType f] (β : SchemeHomOver f f) [IsFinite β.1] [Flat β.1]
    [PreconnectedSpace A] : Function.Surjective β.1

theorem

main

L70 ↗

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

Lean source · statement

theorem main [LocallyOfFiniteType f] (L : RelativeGroupLaw K f) (β : SchemeHomOver f f)
    [IsFinite β.1] [Flat β.1] [PreconnectedSpace A] :
    Function.Surjective β.1 ∧ 0 < L.endDegree β ∧ ∀ x : A, L.endDegree β = β.1.finrank x

theorem

surjective_and_endDegree_eq_finrank_of_isFinite_of_flat

L94 ↗

GoodReductionJacobian.RelativeGroupLaw.surjective_and_endDegree_eq_finrank_of_isFinite_of_flat

Source context 8 commands

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

section ProofImplementation
namespace GoodReductionJacobian.RelativeGroupLaw
noncomputable section
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
open _root_.NeronModelInfra _root_.GoodReductionJacobian
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open RelativeGroupLaw_surjective_and_endDegree_eq_finrank_of_isFinite_of_flat in

Lean source · statement

theorem surjective_and_endDegree_eq_finrank_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] :
    Function.Surjective β.1 ∧ 0 < L.endDegree β ∧
      ∀ x : A, L.endDegree β = Scheme.Hom.finrank β.1 x

Module documentation

Relative Group Law surjective and end Degree eq finrank of is Finite of flat

Declarations

endDegree_eq_finrank_unit

finrank_eq_finrank

endDegree_eq_finrank

one_le_finrank

surjective

main

surjective_and_endDegree_eq_finrank_of_isFinite_of_flat