English
If f is surjective, then dual f is injective (restate of 18943).
Русский
Если f сюръективно, то dual f инъективно.
LaTeX
$$Surjective f ⇒ Injective (dual f)$$
Lean4
/-- For an abelian group `A` and an element `a ∈ A`, there is a character `c : ℤ ∙ a → ℚ ⧸ ℤ` given by
`m • a ↦ m / n` where `n` is the smallest positive integer such that `n • a = 0` and when such `n`
does not exist, `c` is defined by `m • a ↦ m / 2`.
-/
noncomputable def ofSpanSingleton (a : A) : CharacterModule (ℤ ∙ a) :=
let l : ℤ ⧸ Ideal.span {(addOrderOf a : ℤ)} →ₗ[ℤ] AddCircle (1 : ℚ) :=
Submodule.liftQSpanSingleton _
(CharacterModule.int.divByNat <| if addOrderOf a = 0 then 2 else addOrderOf a).toIntLinearMap <|
by
split_ifs with h
· rw [h, Nat.cast_zero, map_zero]
· apply CharacterModule.int.divByNat_self
l ∘ₗ intSpanEquivQuotAddOrderOf a |>.toAddMonoidHom
