English
Given a basis b of G over ℤ, one can construct a corresponding basis of ModN G n over ZMod n.
Русский
По базису b свободного модуля ℤ-G получаем базис ModN G n над ZMod n.
LaTeX
$$basis {ι} (b : Basis ι ℤ G) : Basis ι (ZMod n) (ModN G n)$$
Lean4
/-- Given a free module `G` over `ℤ`, construct the corresponding basis
of `G / ⟨n⟩` over `ℤ / nℤ`. -/
noncomputable def basis {ι : Type*} (b : Basis ι ℤ G) : Basis ι (ZMod n) (ModN G n) :=
by
set ψ : G →+ G := zsmulAddGroupHom n
set nG := LinearMap.range (LinearMap.lsmul ℤ G n)
set H := G ⧸ nG
set φ : G →ₗ[ℤ] H := nG.mkQ
let mod : (ι →₀ ℤ) →ₗ[ℤ] (ι →₀ ZMod n) := mapRange.linearMap (Int.castAddHom _).toIntLinearMap
let f : G →ₗ[ℤ] (ι →₀ ℤ) := b.repr
have hker : nG ≤ LinearMap.ker (mod.comp f) := by
rintro _ ⟨x, rfl⟩
ext b
simp [mod, f]
let g : H →ₗ[ℤ] (ι →₀ ZMod n) := nG.liftQ (mod.comp f) hker
refine ⟨.ofBijective (g.toAddMonoidHom.toZModLinearMap n) ⟨?_, ?_⟩⟩
· rw [AddMonoidHom.coe_toZModLinearMap, LinearMap.toAddMonoidHom_coe, injective_iff_map_eq_zero,
nG.mkQ_surjective.forall]
intro x hx
simp only [Submodule.mkQ_apply, g] at hx
rw [Submodule.liftQ_apply] at hx
replace hx : ∀ b, ↑n ∣ f x b := by simpa [mod, DFunLike.ext_iff, ZMod.intCast_zmod_eq_zero_iff_dvd] using hx
simp only [Submodule.mkQ_apply]
rw [Submodule.Quotient.mk_eq_zero]
choose c hc using hx
refine ⟨b.repr.symm ⟨(f x).support, c, by simp [hc, NeZero.ne]⟩, b.repr.injective ?_⟩
simpa [DFunLike.ext_iff, eq_comm] using hc
· suffices mod ∘ b.repr = g ∘ nG.mkQ by
exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp b.repr.surjective).of_comp
ext x b
simp [mod, g, f, H]
