Module

AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy

14 declarations indexed from sourceView source ↗

Module documentation

Add Comm Group exists mem torsion By smul eq of card torsion By

Imports2

Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Tactic.Positivity

Imported by2

structure

Pres

L30 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres

Documentation

A presentation of the subgroup killed by n as the image of an injective additive map.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function

Lean source · full declaration

structure Pres (M : Type*) [AddCommGroup M] (n : ℕ) (V : Type*) [AddCommGroup V] where
  /-- The additive map presenting the torsion subgroup. -/
  ι : V →+ M
  /-- Injectivity of the presentation map. -/
  hι : Injective ι
  /-- The image consists precisely of the elements killed by `n`. -/
  hιr : ∀ x : M, x ∈ ι.range ↔ ((n : ℕ) : ℤ) • x = 0

theorem

nsmul_ι

L42 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.nsmul_ι

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

theorem nsmul_ι (P : Pres M n V) (v : V) : n • P.ι v = 0

theorem

nsmul_self

L46 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.nsmul_self

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

theorem nsmul_self (P : Pres M n V) (v : V) : n • v = 0

theorem

exists_eq

L49 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.exists_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

theorem exists_eq (P : Pres M n V) {x : M} (hx : n • x = 0) : ∃ v, P.ι v = x

theorem

mem_torsionBy

L53 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.mem_torsionBy

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

theorem mem_torsionBy (P : Pres M n V) (v : V) : P.ι v ∈ torsionBy ℤ M ((n : ℕ) : ℤ)

def

equiv

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.equiv

Documentation

The equivalence between the presented group and the subgroup killed by n.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

def equiv (P : Pres M n V) : V ≃ torsionBy ℤ M ((n : ℕ) : ℤ)

theorem

natCard_eq

L63 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.natCard_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]

Lean source · statement

theorem natCard_eq (P : Pres M n V) : Nat.card V = Nat.card (torsionBy ℤ M ((n : ℕ) : ℤ))

def

self

L68 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.Pres.self

Documentation

The presentation of the torsion subgroup by its inclusion in the ambient group.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]
variable (M) in

Lean source · full declaration

def self (n : ℕ) : Pres M n (torsionBy ℤ M ((n : ℕ) : ℤ)) where
  ι := (torsionBy ℤ M ((n : ℕ) : ℤ)).subtype.toAddMonoidHom
  hι := Subtype.val_injective
  hιr x := by
    constructor
    · rintro ⟨v, rfl⟩
      exact (mem_torsionBy_iff _ _).1 v.2
    · intro hx
      exact ⟨⟨x, (mem_torsionBy_iff _ _).2 hx⟩, rfl⟩

theorem

nsmul_mem_torsionBy_pow

L84 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.nsmul_mem_torsionBy_pow

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
section S
variable {M : Type*} [AddCommGroup M] (ℓ m : ℕ)

Lean source · statement

theorem nsmul_mem_torsionBy_pow {x : M} (hx : x ∈ torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ)) :
    ℓ • x ∈ torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ)

def

mulL

L91 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.mulL

Documentation

Multiplication by ℓ from the torsion of exponent ℓ ^ (m + 1) to that of exponent ℓ ^ m.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
section S
variable {M : Type*} [AddCommGroup M] (ℓ m : ℕ)

Lean source · full declaration

def mulL : torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ) →ₗ[ℤ] torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ) where
  toFun x := ⟨ℓ • (x : M), nsmul_mem_torsionBy_pow ℓ m x.2⟩
  map_add' x y := by
    apply Subtype.ext
    change ℓ • ((x : M) + y) = ℓ • (x : M) + ℓ • (y : M)
    exact smul_add ℓ (x : M) y
  map_smul' c x := by
    apply Subtype.ext
    change ℓ • (c • (x : M)) = c • (ℓ • (x : M))
    exact smul_comm ℓ c (x : M)

theorem

coe_mulL

L102 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.coe_mulL

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
section S
variable {M : Type*} [AddCommGroup M] (ℓ m : ℕ)

Lean source · statement

theorem coe_mulL (x : torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ)) :
    ((mulL ℓ m x : torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ)) : M) = ℓ • (x : M)

theorem

natCard_ker_mulL

L105 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.natCard_ker_mulL

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
section S
variable {M : Type*} [AddCommGroup M] (ℓ m : ℕ)

Lean source · statement

theorem natCard_ker_mulL :
    Nat.card (LinearMap.ker (mulL (M := M) ℓ m)) =
      Nat.card (torsionBy ℤ M ((ℓ ^ 1 : ℕ) : ℤ))

theorem

mulL_surjective

L125 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy.P2mLwS.mulL_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
namespace P2mLwS
open Module Submodule Function
section S
variable {M : Type*} [AddCommGroup M] (ℓ m : ℕ)
variable (r : ℕ)

Lean source · statement

theorem mulL_surjective (hℓ : 0 < ℓ)
    (h1 : Nat.card (torsionBy ℤ M ((ℓ ^ 1 : ℕ) : ℤ)) = (ℓ ^ 1) ^ r)
    (hm : Nat.card (torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ)) = (ℓ ^ m) ^ r)
    (hm1 : Nat.card (torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ)) = (ℓ ^ (m + 1)) ^ r) :
    Surjective (mulL (M := M) ℓ m)

theorem

exists_mem_torsionBy_smul_eq_of_card_torsionBy

L152 ↗

AddCommGroup.exists_mem_torsionBy_smul_eq_of_card_torsionBy

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy

Lean source · statement

theorem _root_.AddCommGroup.exists_mem_torsionBy_smul_eq_of_card_torsionBy (ℓ : ℕ) [Fact ℓ.Prime]
  {M : Type*} [AddCommGroup M] (r m : ℕ)
    (hcard : ∀ j ≤ m + 1, Nat.card (Submodule.torsionBy ℤ M ((ℓ ^ j : ℕ) : ℤ)) = (ℓ ^ j) ^ r)
    (x : M) (hx : x ∈ Submodule.torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ)) :
    ∃ y ∈ Submodule.torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ), ℓ • y = x

Module documentation

Add Comm Group exists mem torsion By smul eq of card torsion By

Declarations