NYLL
Module

AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
29 declarations indexed from sourceView source ↗

Module documentation

Add Comm Group exists basis smul eq of card torsion By

Imports6
Imported by2

Declarations

structure

Pres

L35 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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_ι

L47 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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

L51 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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

L54 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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

L58 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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

L62 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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

L68 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.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_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
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 : ℕ) : ℤ))
theorem

zmod_smul_eq_cast_zsmul

L71 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.Pres.zmod_smul_eq_cast_zsmul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
namespace Pres
variable {M : Type*} [AddCommGroup M] {n : ℕ} {V : Type*} [AddCommGroup V]
Lean source · statement
theorem zmod_smul_eq_cast_zsmul {W : Type*} [AddCommGroup W] [Module (ZMod n) W] (a : ZMod n)
    (w : W) : a • w = (ZMod.cast a : ℤ) • w
theorem

nonempty_basis_of_prime

L78 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.nonempty_basis_of_prime
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
Lean source · statement
theorem nonempty_basis_of_prime {M : Type*} [AddCommGroup M] {N : ℕ} (hN : N.Prime) {r : ℕ}
    {W : Type*} [AddCommGroup W] [Module (ZMod N) W] (P : Pres M N W)
    (hcard : Nat.card (torsionBy ℤ M ((N : ℕ) : ℤ)) = N ^ r) :
    Nonempty (Basis (Fin r) (ZMod N) W)
structure

LiftData

L99 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData
Documentation

Data for lifting a torsion basis from exponent ℓ ^ m to exponent ℓ ^ (m + 1).

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
Lean source · full declaration
structure LiftData (M : Type*) [AddCommGroup M] (ℓ r m : ℕ)
    (V : Type*) [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
    (V' : Type*) [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V'] where
  /-- The presentation at torsion level `ℓ ^ m`. -/
  P : Pres M (ℓ ^ m) V
  /-- The presentation at the next torsion level. -/
  P' : Pres M (ℓ ^ (m + 1)) V'
  /-- The torsion base is positive. -/
  hℓ : 0 < ℓ
  /-- The cardinality of the first torsion level. -/
  h1 : Nat.card (torsionBy ℤ M ((ℓ ^ 1 : ℕ) : ℤ)) = (ℓ ^ 1) ^ r
  /-- The cardinality of the current torsion level. -/
  hm : Nat.card (torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ)) = (ℓ ^ m) ^ r
  /-- The cardinality of the next torsion level. -/
  hm1 : Nat.card (torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ)) = (ℓ ^ (m + 1)) ^ r
  /-- Multiplication by `ℓ` maps the next torsion level onto the current one. -/
  hS : ∀ x ∈ torsionBy ℤ M ((ℓ ^ m : ℕ) : ℤ), ∃ y ∈ torsionBy ℤ M ((ℓ ^ (m + 1) : ℕ) : ℤ), ℓ • y = x
  /-- The basis of the module presenting the current torsion level. -/
  c : Basis (Fin r) (ZMod (ℓ ^ m)) V
theorem

natCard_V'

L121 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.natCard_V'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem natCard_V' (D : LiftData M ℓ r m V V') : Nat.card V' = (ℓ ^ (m + 1)) ^ r
theorem

finite_V'

L124 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.finite_V'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem finite_V' (D : LiftData M ℓ r m V V') : Finite V'
theorem

exists_lift

L127 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.exists_lift
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem exists_lift (D : LiftData M ℓ r m V V') (v : V) : ∃ v' : V', D.P.ι v = ℓ • D.P'.ι v'
def

v'

L134 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.v'
Documentation

A chosen lift of a basis vector to the next torsion level.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
def v' (D : LiftData M ℓ r m V V') (i : Fin r) : V'
theorem

ι_v'

L136 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.ι_v'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem ι_v' (D : LiftData M ℓ r m V V') (i : Fin r) : ℓ • D.P'.ι (D.v' i) = D.P.ι (D.c i)
def

mulBy

L140 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.mulBy
Documentation

The integer-linear map given by multiplication by the natural number k.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
def mulBy (k : ℕ) : V' →ₗ[ℤ] V'
theorem

mulBy_apply

L142 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.mulBy_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem mulBy_apply (k : ℕ) (w : V') : mulBy (V' := V') k w = k • w
theorem

natCard_ker_mulBy

L144 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.natCard_ker_mulBy
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem natCard_ker_mulBy (D : LiftData M ℓ r m V V') {j : ℕ} (hj : j ≤ m + 1) :
    Nat.card (LinearMap.ker (mulBy (V' := V') (ℓ ^ j))) =
      Nat.card (torsionBy ℤ M ((ℓ ^ j : ℕ) : ℤ))
theorem

exists_eq_pow_smul_of_smul_eq_zero

L164 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.exists_eq_pow_smul_of_smul_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem exists_eq_pow_smul_of_smul_eq_zero (D : LiftData M ℓ r m V V') (w : V') (hw : ℓ • w = 0) :
  ∃ z : V', w = ℓ ^ m • z
def

N

L189 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.N
Documentation

The submodule spanned by the chosen lifts of the basis vectors.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
def N (D : LiftData M ℓ r m V V') : Submodule (ZMod (ℓ ^ (m + 1))) V'
theorem

v'_mem_N

L192 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.v'_mem_N
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem v'_mem_N (D : LiftData M ℓ r m V V') (i : Fin r) : D.v' i ∈ D.N
theorem

exists_mem_N_add_smul

L194 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.exists_mem_N_add_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem exists_mem_N_add_smul (D : LiftData M ℓ r m V V') (hm0 : 0 < m) (z : V') : ∃ u ∈ D.N, ∃ z'
  : V', z = u + ℓ • z'
theorem

exists_mem_N_add_pow_smul

L216 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.exists_mem_N_add_pow_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem exists_mem_N_add_pow_smul (D : LiftData M ℓ r m V V') (hm0 : 0 < m) (k : ℕ) (z : V') :
    ∃ u ∈ D.N, ∃ z' : V', z = u + ℓ ^ k • z'
theorem

N_eq_top

L226 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.N_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem N_eq_top (D : LiftData M ℓ r m V V') (hm0 : 0 < m) : D.N = ⊤
theorem

linearIndependent_v'

L232 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.linearIndependent_v'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem linearIndependent_v' (D : LiftData M ℓ r m V V') (hm0 : 0 < m) : LinearIndependent (ZMod (ℓ
  ^ (m + 1))) D.v'
def

liftedBasis

L247 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.liftedBasis
Documentation

The basis at the next torsion level obtained from the chosen lifts.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
def liftedBasis (D : LiftData M ℓ r m V V') (hm0 : 0 < m) : Basis (Fin r) (ZMod (ℓ ^
  (m + 1))) V'
theorem

liftedBasis_apply

L251 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.liftedBasis_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem liftedBasis_apply (D : LiftData M ℓ r m V V') (hm0 : 0 < m) (i : Fin r) : D.liftedBasis hm0
  i = D.v' i
theorem

exists_basis_smul_eq

L255 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy.P2mLwLift.LiftData.exists_basis_smul_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
namespace P2mLwLift
open Module Submodule Function
section Lift
variable {M : Type*} [AddCommGroup M] {ℓ r m : ℕ}
  {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
  {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
namespace LiftData
Lean source · statement
theorem exists_basis_smul_eq (D : LiftData M ℓ r m V V') (hprime : ℓ.Prime) :
    ∃ c' : Basis (Fin r) (ZMod (ℓ ^ (m + 1))) V', ∀ i, D.P.ι (D.c i) = ℓ • D.P'.ι (c' i)
theorem

exists_basis_smul_eq_of_card_torsionBy

L275 ↗
AddCommGroup.exists_basis_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_basis_smul_eq_of_card_torsionBy
Lean source · statement
theorem _root_.AddCommGroup.exists_basis_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)
    {V : Type*} [AddCommGroup V] [Module (ZMod (ℓ ^ m)) V]
    (ι : V →+ M) (hι : Function.Injective ι)
    (hιr : ∀ x : M, x ∈ ι.range ↔ ((ℓ ^ m : ℕ) : ℤ) • x = 0)
    {V' : Type*} [AddCommGroup V'] [Module (ZMod (ℓ ^ (m + 1))) V']
    (ι' : V' →+ M) (hι' : Function.Injective ι')
    (hι'r : ∀ x : M, x ∈ ι'.range ↔ ((ℓ ^ (m + 1) : ℕ) : ℤ) • x = 0)
    (c : Module.Basis (Fin r) (ZMod (ℓ ^ m)) V) :
    ∃ c' : Module.Basis (Fin r) (ZMod (ℓ ^ (m + 1))) V', ∀ i, ι (c i) = ℓ • ι' (c' i)

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