English
χ factors through d iff its unit-map ker is contained in ker of χ.toUnitHom, equivalently the lift factors through via units.
Русский
χ факторизуется через d тогда и только тогда, когда ker единичного отображения больше не содержит элементов вне ker χ.toUnitHom.
LaTeX
$$$$ χ\\text{ factors through } d \\iff \\ker(ZMod.unitsMap\\,d) \\le χ^{\\mathrm{toUnitHom}}.ker. $$$$
Lean4
/-- A Dirichlet character `χ` factors through `d | n` iff its associated unit-group hom is trivial
on the kernel of `ZMod.unitsMap`. -/
theorem factorsThrough_iff_ker_unitsMap {d : ℕ} [NeZero n] (hd : d ∣ n) :
FactorsThrough χ d ↔ (ZMod.unitsMap hd).ker ≤ χ.toUnitHom.ker :=
by
refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩
· rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
· let E := MonoidHom.liftOfSurjective _ (ZMod.unitsMap_surjective hd) ⟨_, h⟩
have hE : E.comp (ZMod.unitsMap hd) = χ.toUnitHom := MonoidHom.liftOfRightInverse_comp ..
refine ⟨hd, MulChar.ofUnitHom E, equivToUnitHom.injective (?_ : toUnitHom _ = toUnitHom _)⟩
simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE, toUnitHom_eq]
