import PaperXI.SmoothDegreeQuotient
import Mathlib.Topology.Algebra.OpenSubgroup
import Mathlib.RepresentationTheory.Subrepresentation
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import PaperXI.LocallyFiniteSemisimple

/-! Smooth representations of compact groups are locally finite dimensional.
This uses compactness of the actual group, not finiteness of the ambient group.
-/
set_option autoImplicit false
noncomputable section
namespace PaperXI.CompactSmoothSemisimple

open Representation PaperXI.SmoothDegreeQuotient
variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
variable (ρ : Representation k G V)

/-- The orbit map factors through the actual vector stabilizer. -/
def orbitQuotient (v : V) : G ⧸ vectorStabilizer ρ v → V :=
  Quotient.lift (fun g => ρ g v) fun g h hgh => by
    have hh : ρ (g⁻¹ * h) v = v := QuotientGroup.leftRel_apply.mp hgh
    calc
      ρ g v = ρ g (ρ (g⁻¹ * h) v) := congrArg (ρ g) hh.symm
      _ = ρ h v := by rw [← Module.End.mul_apply, ← map_mul, mul_inv_cancel_left]

/-- The subrepresentation generated by one vector. -/
def orbitSpan (v : V) : Subrepresentation ρ where
  toSubmodule := Submodule.span k (Set.range fun g => ρ g v)
  apply_mem_toSubmodule g := by
    intro w hw
    induction hw using Submodule.span_induction with
    | mem w hw =>
      obtain ⟨h, rfl⟩ := hw
      apply Submodule.subset_span
      exact ⟨g * h, by simp only [map_mul, Module.End.mul_apply]⟩
    | zero => simp
    | add a b _ _ ha hb => simpa only [map_add] using Submodule.add_mem _ ha hb
    | smul a w _ hw => simpa only [map_smul] using Submodule.smul_mem _ a hw

theorem mem_orbitSpan (v : V) : v ∈ orbitSpan ρ v := by
  apply Submodule.subset_span
  exact ⟨1, by simp⟩

variable [TopologicalSpace G] [IsTopologicalGroup G]

omit [IsTopologicalGroup G] in
/-- Smoothness passes to every subrepresentation. -/
theorem subrepresentation_smooth (hρ : IsSmooth ρ) (S : Subrepresentation ρ) :
    IsSmooth S.toRepresentation := by
  intro v
  have he : (vectorStabilizer S.toRepresentation v : Set G) =
      (vectorStabilizer ρ (v : V) : Set G) := by
    ext g
    exact Subtype.ext_iff
  rw [he]
  exact hρ v

variable [CompactSpace G]

/-- Every smooth orbit under a compact group is finite. -/
theorem orbit_finite (hρ : IsSmooth ρ) (v : V) :
    Set.Finite (Set.range fun g => ρ g v) := by
  let : Finite (G ⧸ vectorStabilizer ρ v) :=
    Subgroup.quotient_finite_of_isOpen _ (hρ v)
  apply (Set.finite_range (orbitQuotient ρ v)).subset
  rintro w ⟨g, rfl⟩
  exact ⟨QuotientGroup.mk g, rfl⟩

/-- Thus each actual orbit-generated subrepresentation is finite dimensional. -/
theorem orbitSpan_finiteDimensional (hρ : IsSmooth ρ) (v : V) :
    FiniteDimensional k (orbitSpan ρ v).toSubmodule :=
  FiniteDimensional.span_of_finite k (orbit_finite ρ hρ v)

/-- A finite-dimensional smooth piece factors through a finite quotient group. -/
theorem subrepresentation_kernel_quotient_finite (hρ : IsSmooth ρ)
    (S : Subrepresentation ρ) [FiniteDimensional k S.toSubmodule] :
    Finite (G ⧸ S.toRepresentation.ker) :=
  Subgroup.quotient_finite_of_isOpen _
    (isOpen_kernel_of_smooth S.toRepresentation (subrepresentation_smooth ρ hρ S))

/-- Every smooth representation of an actual compact group in characteristic
zero is semisimple, including infinite-dimensional smooth representations. -/
theorem smooth_semisimple [CharZero k] (hρ : IsSmooth ρ) :
    IsSemisimpleRepresentation ρ := by
  apply LocallyFiniteSemisimple.semisimple_of_locally_finite_quotient ρ
  intro v
  let S := orbitSpan ρ v
  let : FiniteDimensional k S.toSubmodule := orbitSpan_finiteDimensional ρ hρ v
  exact ⟨S, mem_orbitSpan ρ v, S.toRepresentation.ker, inferInstance,
    subrepresentation_kernel_quotient_finite ρ hρ S, le_rfl⟩

end PaperXI.CompactSmoothSemisimple