Module

Submodule_natCard_torsionBy_quotient_eq_pow_finrank.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_natCard_torsionBy_quotient_eq_pow_finrank

9 declarations indexed from sourceView source ↗

Module documentation

Submodule nat Card torsion By quotient eq pow finrank

Imports1

Mathlib.LinearAlgebra.FreeModule.ModN

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

def

divN

L37 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.divN

Documentation

The additive map given by multiplication by the inverse of the natural-number scalar.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]

Lean source · statement

def divN (n : ℕ) : V →+ V

theorem

natCast_smul_divN

L40 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.natCast_smul_divN

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]

Lean source · statement

theorem natCast_smul_divN {n : ℕ} (hn : n ≠ 0) (v : V) :
    (n : ℤ) • divN (K := K) n v = v

theorem

divN_natCast_smul

L46 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.divN_natCast_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]

Lean source · statement

theorem divN_natCast_smul {n : ℕ} (hn : n ≠ 0) (v : V) :
    divN (K := K) n ((n : ℤ) • v) = v

def

latticeDivQuot

L55 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.latticeDivQuot

Documentation

The map sending a lattice vector divided by the scalar to its torsion class in the quotient.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]
variable (L : Submodule ℤ V)

Lean source · full declaration

def latticeDivQuot {n : ℕ} (hn : n ≠ 0) :
    L →ₗ[ℤ] torsionBy ℤ (V ⧸ L) (n : ℤ) where
  toFun w := ⟨Submodule.Quotient.mk (divN (K := K) n (w : V)), by
    rw [mem_torsionBy_iff]
    change (Submodule.Quotient.mk ((n : ℤ) • divN (K := K) n (w : V)) : V ⧸ L) = 0
    rw [natCast_smul_divN (K := K) hn]
    exact (Submodule.Quotient.mk_eq_zero L).mpr w.2⟩
  map_add' a b := by
    apply Subtype.ext
    change (Submodule.Quotient.mk (divN (K := K) n ((a + b : L) : V)) : V ⧸ L) =
      Submodule.Quotient.mk (divN (K := K) n (a : V))
        + Submodule.Quotient.mk (divN (K := K) n (b : V))
    rw [Submodule.coe_add, map_add, Submodule.Quotient.mk_add]
  map_smul' m a := by
    apply Subtype.ext
    change (Submodule.Quotient.mk (divN (K := K) n ((m • a : L) : V)) : V ⧸ L) =
      Submodule.Quotient.mk (m • divN (K := K) n (a : V))
    rw [Submodule.coe_smul, map_zsmul]

theorem

coe_latticeDivQuot

L74 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.coe_latticeDivQuot

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]
variable (L : Submodule ℤ V)

Lean source · statement

theorem coe_latticeDivQuot {n : ℕ} (hn : n ≠ 0) (w : L) :
    ((latticeDivQuot (K := K) L hn w : torsionBy ℤ (V ⧸ L) (n : ℤ)) : V ⧸ L)
      = Submodule.Quotient.mk (divN (K := K) n (w : V))

theorem

latticeDivQuot_surjective

L78 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.latticeDivQuot_surjective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]
variable (L : Submodule ℤ V)

Lean source · statement

theorem latticeDivQuot_surjective {n : ℕ} (hn : n ≠ 0) :
    Function.Surjective (latticeDivQuot (K := K) L hn)

theorem

ker_latticeDivQuot

L92 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.ker_latticeDivQuot

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]
variable (L : Submodule ℤ V)

Lean source · statement

theorem ker_latticeDivQuot {n : ℕ} (hn : n ≠ 0) :
    LinearMap.ker (latticeDivQuot (K := K) L hn)
      = LinearMap.range (LinearMap.lsmul ℤ L (n : ℤ))

def

latticeQuotTorsionEquiv

L116 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Submodule_natCard_torsionBy_quotient_eq_pow_finrank.Submodule.LatticeQuotientTorsion.latticeQuotTorsionEquiv

Documentation

The equivalence between the lattice modulo the scalar and the scalar-torsion subgroup of its quotient.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_natCard_torsionBy_quotient_eq_pow_finrank
namespace Submodule
open _root_.Submodule
namespace LatticeQuotientTorsion
open _root_.Submodule
open _root_.Submodule
universe u v
variable {K : Type u} [DivisionRing K] [CharZero K]
variable {V : Type v} [AddCommGroup V] [Module K V]
variable (L : Submodule ℤ V)

Lean source · statement

def latticeQuotTorsionEquiv {n : ℕ} (hn : n ≠ 0) :
    ModN L n ≃ₗ[ℤ] torsionBy ℤ (V ⧸ L) (n : ℤ)

theorem

natCard_torsionBy_quotient_eq_pow_finrank

L123 ↗

Submodule.natCard_torsionBy_quotient_eq_pow_finrank

Source context 3 commands

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

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

Lean source · statement

theorem _root_.Submodule.natCard_torsionBy_quotient_eq_pow_finrank
    {K : Type*} [DivisionRing K] [CharZero K]
    {V : Type*} [AddCommGroup V] [Module K V]
    (L : Submodule ℤ V) [Module.Free ℤ L] [Module.Finite ℤ L]
    (n : ℕ) (hn : n ≠ 0) :
    Nat.card (Submodule.torsionBy ℤ (V ⧸ L) (n : ℤ)) = n ^ Module.finrank ℤ L

Module documentation

Submodule nat Card torsion By quotient eq pow finrank

Declarations