NYLL
Module

RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
12 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law is Finite end Ker Str and nat Card eq end Degree of etale

Imports16
Imported by5

Declarations

theorem

locallyQuasiFinite_of_etale

L47 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.locallyQuasiFinite_of_etale
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
Lean source · statement
theorem locallyQuasiFinite_of_etale {X Y : Scheme.{u}} (g : X ⟶ Y) [Etale g] : LocallyQuasiFinite g
theorem

isClosedImmersion_one

L59 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.isClosedImmersion_one
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem isClosedImmersion_one (L : RelativeGroupLaw K f) [IsSeparated f] :
    IsClosedImmersion (L.one (𝟙 (Spec (CommRingCat.of K)))).1
theorem

isClosedImmersion_endKerι

L65 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.isClosedImmersion_endKerι
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem isClosedImmersion_endKerι (L : RelativeGroupLaw K f) [IsSeparated f] (β : SchemeHomOver f
  f) :
    IsClosedImmersion (L.endKerι β)
theorem

isProper_endKerStr

L72 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.isProper_endKerStr
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem isProper_endKerStr (L : RelativeGroupLaw K f) [IsProper f] (β : SchemeHomOver f f) :
    IsProper (L.endKerStr β)
theorem

isFinite_endKerStr

L78 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.isFinite_endKerStr
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem isFinite_endKerStr (L : RelativeGroupLaw K f) [IsProper f] (β : SchemeHomOver f f)
    [Etale (L.endKerStr β)] : IsFinite (L.endKerStr β)
abbrev

KerPts

L85 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.KerPts
Documentation

The points sent to the unit section by the given endomorphism.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
abbrev KerPts (L : RelativeGroupLaw K f) (β : SchemeHomOver f f) : Type u
def

kerPtsEquiv

L90 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.kerPtsEquiv
Documentation

Identify points of the scheme theoretic kernel with points sent to the unit section.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · full declaration
def kerPtsEquiv (L : RelativeGroupLaw K f) (β : SchemeHomOver f f) :
    SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) (L.endKerStr β) ≃ KerPts L β where
  toFun z := ⟨⟨z.1 ≫ L.endKerι β, by
      rw [Category.assoc, RelativeGroupLaw.endKerι_comp_base]; exact z.2⟩, by
      apply Subtype.ext
      change (z.1 ≫ L.endKerι β) ≫ β.1 = (L.one _).1
      rw [Category.assoc, RelativeGroupLaw.endKerι_comp, ← Category.assoc, z.2, Category.id_comp]⟩
  invFun x := ⟨pullback.lift x.1.1 (𝟙 _) (by
      have h := congrArg Subtype.val x.2
      change x.1.1 ≫ β.1 = (L.one _).1 at h
      rw [h, Category.id_comp]), by
      change pullback.lift _ _ _ ≫ pullback.snd _ _ = 𝟙 _
      rw [pullback.lift_snd]⟩
  left_inv z := by
    apply Subtype.ext
    change pullback.lift (z.1 ≫ L.endKerι β) (𝟙 _) _ = z.1
    apply pullback.hom_ext
    · rw [pullback.lift_fst]
    · rw [pullback.lift_snd]; exact z.2.symm
  right_inv x := by
    apply Subtype.ext; apply Subtype.ext
    change pullback.lift x.1.1 (𝟙 _) _ ≫ pullback.fst _ _ = x.1.1
    rw [pullback.lift_fst]
theorem

evalAlgHom_bijective

L118 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.evalAlgHom_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
section Alg
variable (K : Type u) [Field K]
Lean source · full declaration
theorem evalAlgHom_bijective (I : Type u) [Finite I] :
    Function.Bijective (fun i : I => Pi.evalAlgHom K (fun _ : I => K) i) := by
  classical
  let : Fintype I := Fintype.ofFinite I
  let e : I → (I → K) := fun i => Pi.single i 1
  have he : ∀ i k, e i k = if k = i then 1 else 0 := fun i k => by
    simp only [e, Pi.single_apply]
  constructor
  · intro i j hij
    by_contra hne
    have h := congrArg (fun ψ : (I → K) →ₐ[K] K => ψ (e i)) hij
    simp only [Pi.evalAlgHom_apply, he, ite_eq_right (Ne.symm hne)] at h
    exact one_ne_zero h
  · intro ψ
    have hmul : ∀ i j, e i * e j = if i = j then e i else 0 := fun i j => by
      funext k
      simp only [Pi.mul_apply, he]
      split_ifs <;> simp_all
    have hsum1 : ∑ i, e i = 1 := by
      funext k
      rw [Finset.sum_apply, Pi.one_apply, Finset.sum_eq_single k]
      · rw [he, ite_eq_left rfl]
      · intro i _ hik; rw [he, ite_eq_right (Ne.symm hik)]
      · intro h; exact absurd (Finset.mem_univ k) h
    have hsum : ∑ i, ψ (e i) = 1 := by rw [← map_sum, hsum1, map_one]
    obtain ⟨i₀, hi₀⟩ : ∃ i₀, ψ (e i₀) ≠ 0 := by
      by_contra hall
      push Not at hall
      rw [Finset.sum_eq_zero (fun i _ => hall i)] at hsum
      exact zero_ne_one hsum
    have h1 : ψ (e i₀) = 1 := by
      have h : ψ (e i₀) * ψ (e i₀) = ψ (e i₀) * 1 :=
        by rw [← map_mul, hmul, ite_eq_left rfl, mul_one]
      exact mul_left_cancel₀ hi₀ h
    have h0 : ∀ i, i ≠ i₀ → ψ (e i) = 0 := fun i hi => by
      have h : ψ (e i) * ψ (e i₀) = 0 := by rw [← map_mul, hmul, ite_eq_right hi, map_zero]
      rwa [h1, mul_one] at h
    refine ⟨i₀, ?_⟩
    apply AlgHom.ext
    intro v
    have hv : v = ∑ i, v i • e i := by
      funext k
      rw [Finset.sum_apply, Finset.sum_eq_single k]
      · rw [Pi.smul_apply, he, ite_eq_left rfl, smul_eq_mul, mul_one]
      · intro i _ hik; rw [Pi.smul_apply, he, ite_eq_right (Ne.symm hik), smul_zero]
      · intro h; exact absurd (Finset.mem_univ k) h
    change v i₀ = ψ v
    conv_rhs => rw [hv]
    rw [map_sum, Finset.sum_eq_single i₀]
    · rw [map_smul, h1, smul_eq_mul, mul_one]
    · intro i _ hi; rw [map_smul, h0 i hi, smul_zero]
    · intro h; exact absurd (Finset.mem_univ _) h
theorem

finite_and_natCard_algHom_eq_finrank

L173 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.finite_and_natCard_algHom_eq_finrank
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
section Alg
variable (K : Type u) [Field K]
variable [IsAlgClosed K]
Lean source · statement
theorem finite_and_natCard_algHom_eq_finrank (B : Type u) [CommRing B] [Algebra K B]
    [Algebra.FormallyEtale K B] [Module.Finite K B] :
    Finite (B →ₐ[K] K) ∧ Nat.card (B →ₐ[K] K) = Module.finrank K B
theorem

finite_and_natCard_schemeHomOver_eq_finrank

L199 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.finite_and_natCard_schemeHomOver_eq_finrank
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
section Count
variable {K : Type u} [Field K]
Lean source · statement
theorem finite_and_natCard_schemeHomOver_eq_finrank [IsAlgClosed K] {Z : Scheme.{u}}
    (g : Z ⟶ Spec (CommRingCat.of K)) [IsFinite g] [Etale g] :
    Finite (SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) g) ∧
      Nat.card (SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) g) = g.finrank (IsLocalRing.closedPoint
        K)
theorem

main

L259 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mSepKer
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}
Lean source · statement
theorem main [IsAlgClosed K] [IsProper f] (L : RelativeGroupLaw K f) (β : SchemeHomOver f f)
    [Etale (L.endKerStr β)] :
    IsFinite (L.endKerStr β) ∧ Finite (KerPts L β) ∧ Nat.card (KerPts L β) = L.endDegree β
theorem

isFinite_endKerStr_and_natCard_eq_endDegree_of_etale

L269 ↗
GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
Lean source · statement
theorem
  _root_.GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_and_natCard_eq_endDegree_of_etale
    (K : Type u) [Field K] [IsAlgClosed K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
    [IsProper f]
    (L : RelativeGroupLaw K f) (β : SchemeHomOver f f) [Etale (L.endKerStr β)] :
    IsFinite (L.endKerStr β) ∧
      Finite {x : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f //
        NeronModelInfra.schemeHomOverComp x β = L.one (𝟙 (Spec (CommRingCat.of K)))} ∧
      Nat.card {x : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f //
        NeronModelInfra.schemeHomOverComp x β = L.one (𝟙 (Spec (CommRingCat.of K)))} = L.endDegree
          β

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