Module

AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy

8 declarations indexed from sourceView source ↗

Module documentation

Add Comm Group nonempty basis zmod pow of card torsion By

Imports1

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

nsmul_coe_torsionBy

L30 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.nsmul_coe_torsionBy

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]

Lean source · statement

theorem nsmul_coe_torsionBy (k : ℕ) (x : torsionBy ℤ M ((k : ℕ) : ℤ)) : k • (x : M) = 0

def

modInst

L35 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.modInst

Documentation

The action of ZMod k on the subgroup annihilated by multiplication by k.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]

Lean source · statement

def modInst (k : ℕ) : Module (ZMod k) (torsionBy ℤ M ((k : ℕ) : ℤ))

theorem

mem_range_subtype_iff

L42 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.mem_range_subtype_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]
attribute [local instance] modInst

Lean source · statement

theorem mem_range_subtype_iff (k : ℕ) (x : M) :
    x ∈ ((torsionBy ℤ M ((k : ℕ) : ℤ)).subtype.toAddMonoidHom).range ↔ ((k : ℕ) : ℤ) • x = 0

theorem

nonempty_basis_of_subsingleton

L50 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.nonempty_basis_of_subsingleton

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]
attribute [local instance] modInst

Lean source · statement

theorem nonempty_basis_of_subsingleton {R : Type*} [Semiring R] [Subsingleton R] {W : Type*}
    [AddCommMonoid W] [Module R W] [Subsingleton W] (r : ℕ) : Nonempty (Basis (Fin r) R W)

theorem

levelZero

L54 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.levelZero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]
attribute [local instance] modInst

Lean source · statement

theorem levelZero (ℓ r : ℕ) :
    Nonempty (Basis (Fin r) (ZMod (ℓ ^ 0)) (torsionBy ℤ M ((ℓ ^ 0 : ℕ) : ℤ)))

theorem

nonempty_basis_torsionBy

L64 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.nonempty_basis_torsionBy

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]
attribute [local instance] modInst

Lean source · statement

theorem nonempty_basis_torsionBy (ℓ : ℕ) [Fact ℓ.Prime] (r m : ℕ)
    (hcard : ∀ j ≤ m, Nat.card (torsionBy ℤ M ((ℓ ^ j : ℕ) : ℤ)) = (ℓ ^ j) ^ r) :
    ∀ j ≤ m, Nonempty (Basis (Fin r) (ZMod (ℓ ^ j)) (torsionBy ℤ M ((ℓ ^ j : ℕ) : ℤ)))

theorem

nonempty_basis_of_carrier

L81 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy.P2mLwFree.nonempty_basis_of_carrier

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
namespace P2mLwFree
open Module Submodule Function
variable {M : Type*} [AddCommGroup M]
attribute [local instance] modInst

Lean source · statement

theorem nonempty_basis_of_carrier (n : ℕ) {ι' : Type*} (b : Basis ι' (ZMod n) (torsionBy ℤ M ((n :
  ℕ) : ℤ)))
    {V : Type*} [AddCommGroup V] [Module (ZMod n) V]
    (ι : V →+ M) (hι : Function.Injective ι)
    (hιr : ∀ x : M, x ∈ ι.range ↔ ((n : ℕ) : ℤ) • x = 0) :
    Nonempty (Basis ι' (ZMod n) V)

theorem

nonempty_basis_zmod_pow_of_card_torsionBy

L100 ↗

AddCommGroup.nonempty_basis_zmod_pow_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_nonempty_basis_zmod_pow_of_card_torsionBy

Lean source · statement

theorem _root_.AddCommGroup.nonempty_basis_zmod_pow_of_card_torsionBy (ℓ : ℕ) [Fact ℓ.Prime]
    {M : Type*} [AddCommGroup M] (r m : ℕ)
    (hcard : ∀ j ≤ m, 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) :
    Nonempty (Module.Basis (Fin r) (ZMod (ℓ ^ m)) V)

Module documentation

Add Comm Group nonempty basis zmod pow of card torsion By

Declarations