theorem AddChar.map_eq_one_of_mem_closure {G : Type u_2} [AddCommGroup G] {Δ : Set (AddChar G ℂ)} {ψ : AddChar G ℂ} {x : G} (hψ : ψ ∈ AddSubgroup.closure Δ) (hx : ∀ γ ∈ Δ, γ x = 1) : ψ x = 1

@[simp]

theorem AddChar.map_doubleDualEquiv_symm {G : Type u_2} [AddCommGroup G] [Finite G] (χ : AddChar (AddChar G ℂ) ℂ) (ψ : AddChar G ℂ) : ψ (doubleDualEquiv.symm χ) = χ ψ

theorem AddChar.mem_closure_iff {G : Type u_2} [AddCommGroup G] {Δ : Set (AddChar G ℂ)} {ψ : AddChar G ℂ} [Finite G] : ψ ∈ AddSubgroup.closure Δ ↔ ∀ (x : G), (∀ γ ∈ Δ, γ x = 1) → ψ x = 1

theorem AddChar.expect_iInf_ker_eq_one_of_mem_closure {G : Type u_2} [AddCommGroup G] {Δ : Set (AddChar G ℂ)} {ψ : AddChar G ℂ} {V : AddSubgroup G} [Fintype ↥V] (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker) (hψ : ψ ∈ AddSubgroup.closure Δ) : ((↑V).toFinset.expect fun (x : G) => ψ x) = 1

theorem AddChar.expect_iInf_ker_eq_zero_of_not_mem_closure {G : Type u_2} [AddCommGroup G] {Δ : Set (AddChar G ℂ)} {ψ : AddChar G ℂ} [Finite G] {V : AddSubgroup G} [Fintype ↥V] (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker) (hψ : ψ ∉ AddSubgroup.closure Δ) : ((↑V).toFinset.expect fun (x : G) => ψ x) = 0

noncomputable def AddChar.toZModLinearMap {G : Type u_2} (q : ℕ) [AddCommGroup G] [Module (ZMod q) G] (γ : AddChar G ℂ) [NeZero q] : G →ₗ[ZMod q] ZMod q

Characters of a q-group G are (noncanonically) the same as ZMod q-linear forms on G.

Equations

• AddChar.toZModLinearMap q γ = AddMonoidHom.toZModLinearMap q (AddChar.zmodAddEquiv.symm.toAddMonoidHom.comp γ.toAddMonoidHomAddChar)

theorem AddChar.toZModLinearMap_apply {G : Type u_2} (q : ℕ) [AddCommGroup G] [Module (ZMod q) G] (γ : AddChar G ℂ) [NeZero q] (a✝ : G) : (toZModLinearMap q γ) a✝ = zmodAddEquiv.symm (γ.toAddMonoidHomAddChar a✝)

@[simp]

theorem AddChar.toZModLinearMap_eq_zero {G : Type u_2} {q : ℕ} [AddCommGroup G] [Module (ZMod q) G] {γ : AddChar G ℂ} {x : G} [Fact (1 < q)] : (toZModLinearMap q γ) x = 0 ↔ γ x = 1

@[simp]

theorem AddChar.ker_toZModLinearMap {G : Type u_2} {q : ℕ} [AddCommGroup G] [Module (ZMod q) G] {γ : AddChar G ℂ} [Fact (1 < q)] : (toZModLinearMap q γ).ker = (AddSubgroup.toZModSubmodule q) γ.toAddMonoidHom.ker

theorem AddChar.codim_iInf_ker_le_fintypeCard {ι : Type u_1} {G : Type u_2} {q : ℕ} [AddCommGroup G] [Module (ZMod q) G] [Fact (Nat.Prime q)] [FiniteDimensional (ZMod q) G] {γ : ι → AddChar G ℂ} [Fintype ι] : Module.finrank (ZMod q) G - (⨅ (i : ι), (AddSubgroup.toZModSubmodule q) (γ i).toAddMonoidHom.ker).finrank ≤ Fintype.card ι

theorem AddChar.codim_iInf_ker_le_finsetCard {ι : Type u_1} {G : Type u_2} {q : ℕ} [AddCommGroup G] [Module (ZMod q) G] [Fact (Nat.Prime q)] [FiniteDimensional (ZMod q) G] {γ : ι → AddChar G ℂ} {s : Finset ι} : Module.finrank (ZMod q) G - ((AddSubgroup.toZModSubmodule q) (⨅ i ∈ s, (γ i).toAddMonoidHom.ker)).finrank ≤ s.card