@[reducible, inline]

abbrev CharacterTheory.HomG {k : Type u} [CommRing k] {G : Type u} [Monoid G] {V : Type u} [AddCommMonoid V] [Module k V] {W : Type u} [AddCommMonoid W] [Module k W] (ρ : Representation k G V) (ψ : Representation k G W) : Type u

theorem CharacterTheory.schur_dim_HomG {k : Type u} [Field k] [IsAlgClosed k] {G : Type u} [Group G] [Fintype G] [Invertible ↑(Nat.card G)] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {W : Type u} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [ρ.IsIrreducible] [σ.IsIrreducible] : Module.finrank k (HomG ρ σ) = if Nonempty (σ.Equiv ρ) then 1 else 0

theorem CharacterTheory.rep_convolution_eq_comp {k : Type u} [Field k] {G : Type u} [Group G] [Fintype G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (φ ψ : MonoidAlgebra k G) : ρ.asAlgebraHom (φ * ψ) = ρ.asAlgebraHom φ * ρ.asAlgebraHom ψ

def CharacterTheory.convolution {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {k : Type u_2} [CommSemiring k] (φ ψ : G → k) : G → k

def CharacterTheory.IsClassFunction {G : Type u} [Group G] {k : Type u} [Field k] (f : G → k) : Prop

noncomputable def CharacterTheory.classInnerProduct {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [Invertible ↑(Nat.card G)] (f₁ f₂ : G → k) : k

theorem CharacterTheory.character_orthonormality {G : Type u} [Group G] {k : Type u} [Field k] {V W : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [ρ.IsIrreducible] [σ.IsIrreducible] : classInnerProduct ρ.character σ.character = if Nonempty (σ.Equiv ρ) then 1 else 0

theorem CharacterTheory.character_selfInnerProduct_eq_sum_sq_aux {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [Invertible ↑(Nat.card G)] [IsAlgClosed k] {ι : Type u} [Fintype ι] [DecidableEq ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h_pairwise : ∀ (i j : ι), i ≠ j → ¬Nonempty ((ρ i).Equiv (ρ j))) (n : ι → ℕ) (χ : G → k) (hχ : ∀ (g : G), χ g = ∑ i : ι, ↑(n i) * (ρ i).character g) : classInnerProduct χ χ = ∑ i : ι, ↑(n i) ^ 2

theorem CharacterTheory.isIrreducible_of_finrank_intertwiningMap_eq_one {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] [IsAlgClosed k] (σ : Representation k G V) (hfr : Module.finrank k (σ.IntertwiningMap σ) = 1) : σ.IsIrreducible

theorem CharacterTheory.character_selfInnerProduct_irreducible_iff_aux {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [CharZero k] (σ : Representation k G V) : σ.IsIrreducible ↔ classInnerProduct σ.character σ.character = 1

theorem CharacterTheory.character_selfInnerProduct_corollary {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [CharZero k] {ι : Type u} [Fintype ι] [DecidableEq ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h_pairwise : ∀ (i j : ι), i ≠ j → ¬Nonempty ((ρ i).Equiv (ρ j))) (n : ι → ℕ) (χ : G → k) (hχ : ∀ (g : G), χ g = ∑ i : ι, ↑(n i) * (ρ i).character g) : classInnerProduct χ χ = ∑ i : ι, ↑(n i) ^ 2 ∧ ∀ {W : Type u} [inst : AddCommGroup W] [inst_1 : Module k W] [FiniteDimensional k W] (σ : Representation k G W), σ.IsIrreducible ↔ classInnerProduct σ.character σ.character = 1

theorem CharacterTheory.mainTheorem_wedderburn (k : Type u) [Field k] [IsAlgClosed k] (G : Type u) [Group G] [Fintype G] [NeZero ↑(Nat.card G)] : ∃ (n : ℕ) (d : Fin n → ℕ), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (MonoidAlgebra k G ≃ₐ[k] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) k)

theorem CharacterTheory.mainTheorem_sum_sq_eq_card (k : Type u) [Field k] [IsAlgClosed k] (G : Type u) [Group G] [Fintype G] [NeZero ↑(Nat.card G)] : ∃ (n : ℕ) (d : Fin n → ℕ), (∀ (i : Fin n), NeZero (d i)) ∧ ∑ i : Fin n, d i ^ 2 = Nat.card G ∧ Nonempty (MonoidAlgebra k G ≃ₐ[k] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) k)

theorem CharacterTheory.rat_int_of_pow_int (r : ℚ) (d : ℤ) (hd : d ≠ 0) (h : ∀ (n : ℕ), ∃ (m : ℤ), ↑d * r ^ n = ↑m) : ∃ (z : ℤ), r = ↑z

theorem CharacterTheory.mainTheorem_characters_span {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [IsAlgClosed k] [NeZero ↑(Nat.card G)] (f : G → k) (hf : IsClassFunction f) (horth : ∀ (V : Type u) [inst : AddCommGroup V] [inst_1 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible], (↑(Nat.card G))⁻¹ * ∑ g : G, f g * ρ.character g⁻¹ = 0) : f = 0

theorem CharacterTheory.char_charpoly_roots_pow_eq_one {G : Type u} [Group G] [Fintype G] {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) (μ : ℂ) : μ ∈ ((LinearMap.toMatrix (Module.finBasis ℂ V) (Module.finBasis ℂ V)) (ρ g)).charpoly.roots → μ ^ Fintype.card G = 1

theorem CharacterTheory.char_inv_eq_conj {G : Type u} [Group G] [Fintype G] {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) : ρ.character g⁻¹ = (starRingEnd ℂ) (ρ.character g)

theorem CharacterTheory.char_dual_eq_conj {G : Type u} [Group G] [Fintype G] {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) : ρ.dual.character g = (starRingEnd ℂ) (ρ.character g)

theorem CharacterTheory.char_value_properties {G : Type u} [Group G] [Fintype G] {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) : (∀ μ ∈ ((LinearMap.toMatrix (Module.finBasis ℂ V) (Module.finBasis ℂ V)) (ρ g)).charpoly.roots, μ ^ Fintype.card G = 1) ∧ ρ.character g⁻¹ = (starRingEnd ℂ) (ρ.character g) ∧ ρ.dual.character g = (starRingEnd ℂ) (ρ.character g)

theorem CharacterTheory.abelian_irrep_one_dimensional {k : Type u_1} [Field k] [IsAlgClosed k] {G : Type u_2} [CommGroup G] [Finite G] {V : Type u_3} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (hirr : ρ.IsIrreducible) : Module.finrank k V = 1

theorem CharacterTheory.multiplicity_eq_finrank_intertwining {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [Field k] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h_pairwise : ∀ (i j : ι), i ≠ j → ¬Nonempty ((ρ i).Equiv (ρ j))) {W : Type u_5} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) (d : ι → ℕ) (h_decomp : Nonempty (σ.Equiv (Representation.directSum fun (p : (i : ι) × Fin (d i)) => ρ p.fst))) (i : ι) : d i = Module.finrank k ((ρ i).IntertwiningMap σ)

theorem CharacterTheory.maschke_irreducible_decomposition {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [Field k] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h_complete : ∀ (U : Type u_5) [inst : AddCommGroup U] [inst_1 : Module k U] [FiniteDimensional k U] (τ : Representation k G U), τ.IsIrreducible → ∃ (i : ι), Nonempty (τ.Equiv (ρ i))) {W : Type u_6} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) : ∃ (d : ι → ℕ), Nonempty (σ.Equiv (Representation.directSum fun (p : (i : ι) × Fin (d i)) => ρ p.fst))

theorem CharacterTheory.decomposition_corollary {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [Field k] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h_pairwise : ∀ (i j : ι), i ≠ j → ¬Nonempty ((ρ i).Equiv (ρ j))) (h_complete : ∀ (U : Type u_5) [inst : AddCommGroup U] [inst_1 : Module k U] [FiniteDimensional k U] (τ : Representation k G U), τ.IsIrreducible → ∃ (i : ι), Nonempty (τ.Equiv (ρ i))) {W : Type u_6} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) : ∃ (d : ι → ℕ), Nonempty (σ.Equiv (Representation.directSum fun (p : (i : ι) × Fin (d i)) => ρ p.fst)) ∧ ∀ (i : ι), d i = Module.finrank k ((ρ i).IntertwiningMap σ)

noncomputable def CharacterTheory.repOfFun {k : Type u_1} [Field k] {G : Type u_2} [Group G] [Fintype G] {V : Type u_3} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (f : G → k) : V →ₗ[k] V

theorem CharacterTheory.monoidAlgebra_pow_isIntegral {G : Type u_1} [Group G] [Fintype G] (φ : MonoidAlgebra ℂ G) (hφ : ∀ (g : G), IsIntegral ℤ (φ g)) (n : ℕ) (g : G) : IsIntegral ℤ ((φ ^ n) g)

theorem CharacterTheory.repOfFun_eq_asAlgebraHom {G : Type u_1} [Group G] [Fintype G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) (f : G → ℂ) : repOfFun ρ f = ρ.asAlgebraHom (Finsupp.equivFunOnFinite.symm f)

theorem CharacterTheory.char_isIntegral {G : Type u_1} [Group G] [Fintype G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (g : G) : IsIntegral ℤ ((LinearMap.trace ℂ V) (ρ g))

theorem CharacterTheory.repOfFun_scalar_rational_is_int {G : Type u_1} [Group G] [Fintype G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (f : G → ℂ) (r : ℚ) (hf : ∀ (g : G), IsIntegral ℤ (f g)) (hρf : repOfFun ρ f = (algebraMap ℚ ℂ) r • LinearMap.id) (hdim : Module.finrank ℂ V ≠ 0) : ∃ (z : ℤ), r = ↑z

theorem CharacterTheory.repOfFun_comm_of_classFunction {k : Type u_1} [Field k] {G : Type u_2} [Group G] [Fintype G] {V : Type u_3} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (f : G → k) (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) (h : G) : repOfFun ρ f ∘ₗ ρ h = ρ h ∘ₗ repOfFun ρ f

theorem CharacterTheory.irred_rep_class_fun_scalar {k : Type u_1} [Field k] [IsAlgClosed k] {G : Type u_2} [Group G] [Fintype G] {V : Type u_3} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] (f : G → k) (hf : ∀ (g h : G), f (h * g * h⁻¹) = f g) : ∃ (c : k), repOfFun ρ f = c • LinearMap.id

theorem CharacterTheory.rep_conj_char_eq_scalar {k : Type u_1} [Field k] [IsAlgClosed k] {G : Type u_2} [Group G] [Fintype G] [Invertible ↑(Nat.card G)] {V : Type u_3} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : ∃ (c : k), (repOfFun ρ fun (g : G) => ρ.character g⁻¹) = c • LinearMap.id ∧ c * ↑(Module.finrank k V) = ↑(Nat.card G)

theorem CharacterTheory.monoidAlgebra_pow_isIntegral_general {k : Type u_1} [Field k] {G : Type u_2} [Group G] [Fintype G] (φ : MonoidAlgebra k G) (hφ : ∀ (g : G), IsIntegral ℤ (φ g)) (n : ℕ) (g : G) : IsIntegral ℤ ((φ ^ n) g)

theorem CharacterTheory.char_isIntegral_general {k : Type u_1} [Field k] [IsAlgClosed k] {G : Type u_2} [Group G] [Fintype G] {V : Type u_3} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (g : G) : IsIntegral ℤ ((LinearMap.trace k V) (ρ g))

theorem CharacterTheory.mainTheorem_dim_dvd_card_charZero {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] [NeZero ↑(Nat.card G)] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : Module.finrank k V ∣ Nat.card G

theorem CharacterTheory.irred_dim_dvd_card {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] [NeZero ↑(Nat.card G)] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] : Module.finrank k V ∣ Fintype.card G

noncomputable def CharacterTheory.wedderburnIrrep (k : Type u) [Field k] [IsAlgClosed k] (G : Type u) [Group G] [Fintype G] [NeZero ↑(Nat.card G)] {n : ℕ} {d : Fin n → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (j : Fin n) → Matrix (Fin (d j)) (Fin (d j)) k) (i : Fin n) : Representation k G (Fin (d i) → k)

theorem CharacterTheory.wedderburnIrrep_isIrreducible (k : Type u) [Field k] [IsAlgClosed k] (G : Type u) [Group G] [Fintype G] [NeZero ↑(Nat.card G)] {n : ℕ} {d : Fin n → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (j : Fin n) → Matrix (Fin (d j)) (Fin (d j)) k) (i : Fin n) [NeZero (d i)] : (wedderburnIrrep k G e i).IsIrreducible

theorem CharacterTheory.mainTheorem (G : Type u) [Group G] [Fintype G] (k : Type u) [Field k] [IsAlgClosed k] [CharZero k] [NeZero ↑(Nat.card G)] : (∀ (f : G → k), IsClassFunction f → (∀ (V : Type u) [inst : AddCommGroup V] [inst_1 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible], (↑(Nat.card G))⁻¹ * ∑ g : G, f g * ρ.character g⁻¹ = 0) → f = 0) ∧ (∀ (V W : Type u) [inst : AddCommGroup V] [inst_1 : Module k V] [FiniteDimensional k V] [inst_3 : AddCommGroup W] [inst_4 : Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [ρ.IsIrreducible] [σ.IsIrreducible], (↑(Nat.card G))⁻¹ * ∑ g : G, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0) ∧ (∃ (n : ℕ) (d : Fin n → ℕ), (∀ (i : Fin n), 0 < d i) ∧ (∀ (i : Fin n), ∃ (V : Type u) (x : AddCommGroup V) (x_1 : Module k V) (_ : FiniteDimensional k V) (ρ : Representation k G V), ρ.IsIrreducible ∧ Module.finrank k V = d i) ∧ ∑ i : Fin n, d i ^ 2 = Nat.card G) ∧ ∀ (V : Type u) [inst : AddCommGroup V] [inst_1 : Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible], Module.finrank k V ∣ Nat.card G