Documentation

TauCeti.Data.ZMod.MulCastHom

Multiplication by k from ZMod m to ZMod (m * k) #

For natural numbers m, k and n = m * k, multiplication by k is a well-defined additive homomorphism ZMod m →+ ZMod n: the class of an integer a modulo m goes to the class of a * k modulo n. Together with the reduction ZMod.castHom : ZMod n →+* ZMod k it forms, for k ≠ 0, the short exact sequence of cyclic groups

0 → ZMod m → ZMod n → ZMod k → 0

since multiplication by k ≠ 0 is injective, the reduction is surjective, and the classes killed by the reduction are exactly the multiples of k (for k = 0 the multiplication is the zero map, and only the exactness at ZMod n and the surjectivity survive). The multiplications compose, and they commute with the reductions. The instance of interest is m = pⁱ, k = pʲ, n = pⁱ⁺ʲ, which gives the sequences 0 → ℤ/pⁱ → ℤ/pⁱ⁺ʲ → ℤ/pʲ → 0 of the coefficient systems of p-adic characters.

Main definitions #

Main results #

source
def ZMod.mulCastHom {m n : ℕ} (k : ℕ) (h : m * k = n) :
ZMod m →+ ZMod n

Multiplication by k, ZMod m →+ ZMod n for n = m * k: the class of an integer a modulo m goes to the class of a * k modulo n.

Equations
Instances For
    source
    @[simp]
    theorem ZMod.mulCastHom_intCast {m n : ℕ} (k : ℕ) (h : m * k = n) (a : ℤ) :
    (mulCastHom k h) ↑a = ↑a * ↑k

    Multiplication by k on the class of an integer a is the class of a * k.

    source
    theorem ZMod.mulCastHom_apply {m n : ℕ} (k : ℕ) (h : m * k = n) (a : ZMod m) :
    (mulCastHom k h) a = a.cast * ↑k

    Multiplication by k sends a class to k times its cast, for any representative.

    source
    theorem ZMod.mulCastHom_injective {m n : ℕ} (k : ℕ) (h : m * k = n) (hk : k ≠ 0) :
    Function.Injective ⇑(mulCastHom k h)

    Multiplication by k ≠ 0 is injective on ZMod m: if m * k ∣ a * k then m ∣ a.

    source
    @[simp]
    theorem ZMod.mulCastHom_one {m : ℕ} :
    mulCastHom 1 ⋯ = AddMonoidHom.id (ZMod m)

    Multiplication by 1 is the identity.

    source
    theorem ZMod.mulCastHom_mulCastHom {m n : ℕ} (k : ℕ) (h : m * k = n) {n₂ : ℕ} (k₂ : ℕ) (h₂ : n * k₂ = n₂) (h₁₂ : m * (k * k₂) = n₂) (a : ZMod m) :
    (mulCastHom k₂ h₂) ((mulCastHom k h) a) = (mulCastHom (k * k₂) h₁₂) a

    Two successive multiplications, by k and then by k₂, compose to the multiplication by k * k₂. The index equation of the composite is taken as a hypothesis, so that any proof of it may be used.

    source
    theorem ZMod.mulCastHom_castHom_mul {m n : ℕ} (k : ℕ) (h : m * k = n) (b : ZMod n) (a : ZMod m) :
    (mulCastHom k h) ((castHom ⋯ (ZMod m)) b * a) = b * (mulCastHom k h) a

    Multiplication by k is semilinear for the reduction ZMod n → ZMod m: scaling a class of ZMod m by the reduction of b : ZMod n and then multiplying by k is scaling the result by b.

    source
    theorem ZMod.castHom_mulCastHom {m n : ℕ} (k : ℕ) (h : m * k = n) (a : ZMod m) :
    (castHom ⋯ (ZMod k)) ((mulCastHom k h) a) = 0

    The reduction modulo k kills the multiples of k.

    source
    @[simp]
    theorem ZMod.cast_mulCastHom {m n : ℕ} (k : ℕ) (h : m * k = n) (a : ZMod m) :
    ((mulCastHom k h) a).cast = 0

    The cast of a multiple of k to ZMod k vanishes: the simp normal form of castHom_mulCastHom.

    source
    theorem ZMod.exact_mulCastHom_castHom {m n : ℕ} (k : ℕ) (h : m * k = n) :
    Function.Exact ⇑(mulCastHom k h) ⇑(castHom ⋯ (ZMod k))

    Exactness of ZMod m → ZMod n → ZMod k: the classes modulo n = m * k killed by the reduction modulo k are exactly the multiples of k.

    source
    theorem ZMod.castHom_mulCastHom_eq_mulCastHom_castHom {m n : ℕ} (k : ℕ) (h : m * k = n) {m' n' : ℕ} (h' : m' * k = n') (hm : m' ∣ m) (hn : n' ∣ n) (a : ZMod m) :
    (castHom hn (ZMod n')) ((mulCastHom k h) a) = (mulCastHom k h') ((castHom hm (ZMod m')) a)

    The reductions commute with the multiplications: reducing k * a modulo n' is k times the reduction of a modulo m', for m' * k = n'. Both divisibilities are hypotheses, so that any proofs of them may be used.