From 14bd4f65b4f45e7747da8e4c0d90d02a58dec086 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Javier=20L=C3=B3pez-Contreras?=
 <38789151+javierlcontreras@users.noreply.github.com>
Date: Sat, 21 Dec 2024 17:06:11 +0100
Subject: [PATCH] feat(RepresentationTheory): Adds Subrepresentation,
 Representation.Irreducible (#286)

---
 .../RepresentationTheory/Irreducible.lean     | 30 ++++++++
 .../Subrepresentation.lean                    | 74 +++++++++++++++++++
 FLT/Mathlib/LinearAlgebra/Span/Defs.lean      | 28 +++++++
 FLT/Mathlib/RepresentationTheory/Basic.lean   | 38 ++++++++++
 4 files changed, 170 insertions(+)
 create mode 100644 FLT/Deformations/RepresentationTheory/Irreducible.lean
 create mode 100644 FLT/Deformations/RepresentationTheory/Subrepresentation.lean
 create mode 100644 FLT/Mathlib/LinearAlgebra/Span/Defs.lean
 create mode 100644 FLT/Mathlib/RepresentationTheory/Basic.lean

diff --git a/FLT/Deformations/RepresentationTheory/Irreducible.lean b/FLT/Deformations/RepresentationTheory/Irreducible.lean
new file mode 100644
index 00000000..437ba2e8
--- /dev/null
+++ b/FLT/Deformations/RepresentationTheory/Irreducible.lean
@@ -0,0 +1,30 @@
+import FLT.Deformations.RepresentationTheory.Subrepresentation
+import FLT.Mathlib.RepresentationTheory.Basic
+
+namespace Representation
+
+variable {G : Type*} [Group G]
+
+variable {k : Type*} [Field k]
+
+variable {W : Type*} [AddCommMonoid W] [Module k W]
+
+/-!
+  `IsIrreducible ρ` is the statement that a given Representation ρ is irreducible (also known as simple),
+  meaning that any subrepresentation must be either the full one (⊤) or zero (⊥)
+
+  This notion is only well behaved when the representation is over a field k. If it were defined over
+  a ring A with a nontrivial ideal J, the subrepresentation JW would often be a non trivial subrepresentation,
+  so ρ would rarely be irreducible.
+-/
+class IsIrreducible (ρ : Representation k G W) : Prop where
+  irreducible : IsSimpleOrder (Subrepresentation ρ)
+
+/-!
+  `IsAbsolutelyIrreducible ρ` states that a given Representation ρ over a field k
+  is absolutely irreducible, meaning that all the possible base change extensions are irreducible.
+-/
+class IsAbsolutelyIrreducible (ρ : Representation k G W) : Prop where
+  absolutelyIrreducible : ∀ k', ∀ _ : Field k', ∀ _ : Algebra k k', IsIrreducible (k' ⊗ᵣ' ρ)
+
+end Representation
diff --git a/FLT/Deformations/RepresentationTheory/Subrepresentation.lean b/FLT/Deformations/RepresentationTheory/Subrepresentation.lean
new file mode 100644
index 00000000..98095724
--- /dev/null
+++ b/FLT/Deformations/RepresentationTheory/Subrepresentation.lean
@@ -0,0 +1,74 @@
+import Mathlib.RepresentationTheory.Basic
+import FLT.Mathlib.LinearAlgebra.Span.Defs
+
+open Pointwise
+
+universe u
+
+variable {A : Type*} [CommRing A]
+
+variable {G : Type*} [Group G]
+
+variable {W : Type*} [AddCommMonoid W] [Module A W]
+
+variable {ρ : Representation A G W}
+
+variable (ρ) in
+structure Subrepresentation where
+  toSubmodule : Submodule A W
+  apply_mem_toSubmodule (g : G) ⦃v : W⦄ : v ∈ toSubmodule → ρ g v ∈ toSubmodule
+
+namespace Subrepresentation
+
+lemma toSubmodule_injective : Function.Injective (toSubmodule : Subrepresentation ρ → Submodule A W) := by
+  rintro ⟨_,_⟩
+  congr!
+
+instance : SetLike (Subrepresentation ρ) W where
+  coe ρ' := ρ'.toSubmodule
+  coe_injective' := SetLike.coe_injective.comp toSubmodule_injective
+
+def toRepresentation (ρ' : Subrepresentation ρ): Representation A G ρ'.toSubmodule where
+  toFun g := (ρ g).restrict (ρ'.apply_mem_toSubmodule g)
+  map_one' := by ext; simp
+  map_mul' x y := by ext; simp
+
+instance : Max (Subrepresentation ρ) where
+  max ρ₁ ρ₂ := .mk (ρ₁.toSubmodule ⊔ ρ₂.toSubmodule) <| by
+      simp only [Submodule.forall_mem_sup, map_add]
+      intro g x₁ hx₁ x₂ hx₂
+      exact Submodule.mem_sup.mpr
+        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩
+
+instance : Min (Subrepresentation ρ) where
+  min ρ₁ ρ₂ := .mk (ρ₁.toSubmodule ⊓ ρ₂.toSubmodule) <| by
+      simp only [Submodule.mem_inf, and_imp]
+      rintro g x hx₁ hx₂
+      exact ⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩
+
+
+@[simp, norm_cast]
+lemma coe_sup (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊔ ρ₂) = (ρ₁ : Set W) + (ρ₂ : Set W) :=
+  Submodule.coe_sup ρ₁.toSubmodule ρ₂.toSubmodule
+
+@[simp, norm_cast]
+lemma coe_inf (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊓ ρ₂) = (ρ₁ ∩ ρ₂ : Set W) := rfl
+
+@[simp]
+lemma toSubmodule_sup (ρ₁ ρ₂ : Subrepresentation ρ) :
+  (ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule := rfl
+
+@[simp]
+lemma toSubmodule_inf (ρ₁ ρ₂ : Subrepresentation ρ) :
+  (ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule := rfl
+
+instance : Lattice (Subrepresentation ρ) :=
+  toSubmodule_injective.lattice _ toSubmodule_sup toSubmodule_inf
+
+instance : BoundedOrder (Subrepresentation ρ) where
+  top := ⟨⊤, by simp⟩
+  le_top _ _ := by simp
+  bot := ⟨⊥, by simp⟩
+  bot_le _ _ := by simp +contextual
+
+end Subrepresentation
diff --git a/FLT/Mathlib/LinearAlgebra/Span/Defs.lean b/FLT/Mathlib/LinearAlgebra/Span/Defs.lean
new file mode 100644
index 00000000..c45602ed
--- /dev/null
+++ b/FLT/Mathlib/LinearAlgebra/Span/Defs.lean
@@ -0,0 +1,28 @@
+import Mathlib.LinearAlgebra.Span.Defs
+
+open Pointwise
+
+variable {R : Type*} [Semiring R]
+
+variable {M : Type*} [AddCommMonoid M] [Module R M]
+
+variable {p p' : Submodule R M}
+
+variable {P : M → Prop}
+
+namespace Submodule
+
+@[simp high]
+lemma forall_mem_sup : (∀ x ∈ p ⊔ p', P x) ↔ (∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)) := by
+  simp [mem_sup]
+  aesop
+
+@[simp high]
+lemma exists_mem_sup : (∃ x ∈ p ⊔ p', P x) ↔ (∃ x₁ ∈ p, ∃ x₂ ∈ p', P (x₁ + x₂)) := by
+  simp [mem_sup]
+
+@[simp, norm_cast]
+lemma coe_sup' : ↑(p ⊔ p') = (p : Set M) + (p' : Set M) := by
+  simp [coe_sup]
+
+end Submodule
diff --git a/FLT/Mathlib/RepresentationTheory/Basic.lean b/FLT/Mathlib/RepresentationTheory/Basic.lean
new file mode 100644
index 00000000..c8a381b1
--- /dev/null
+++ b/FLT/Mathlib/RepresentationTheory/Basic.lean
@@ -0,0 +1,38 @@
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
+import Mathlib.RepresentationTheory.Basic
+
+open LinearMap
+open scoped TensorProduct
+
+namespace Representation
+
+variable {R V G ι: Type*} [CommRing R] [AddCommMonoid V] [Module R V] [Module.Free R V]
+  [Module.Finite R V] [Group G] [DecidableEq ι] [Fintype ι]
+
+variable (ρ : Representation R G V) (𝓑 : Basis ι R V)
+
+omit [Module.Free R V] [Module.Finite R V] in
+@[simp]
+lemma comp_def (g h : G): ρ g ∘ₗ ρ h = ρ g * ρ h := rfl
+
+noncomputable def gl_map_of_basis
+  : G →* Matrix.GeneralLinearGroup ι R where
+    toFun g := {
+      val := LinearMap.toMatrix 𝓑 𝓑 (ρ g)
+      inv := LinearMap.toMatrix 𝓑 𝓑 (ρ g⁻¹)
+      val_inv := by rw [← toMatrix_comp, comp_def, ← map_mul]; simp
+      inv_val := by rw [← toMatrix_comp, comp_def, ← map_mul]; simp
+    }
+    map_one' := by aesop
+    map_mul' := by rintro x y; simp [LinearMap.toMatrix_mul]; norm_cast
+
+noncomputable def baseChange (R' : Type*) [CommRing R'] [Algebra R R'] (ρ : Representation R G V)
+    : Representation R' G (R' ⊗[R] V) where
+  toFun g := LinearMap.baseChange R' (ρ g)
+  map_one' := by aesop
+  map_mul' := by aesop
+
+scoped notation ρ "⊗ᵣ" ρ' => tprod ρ ρ'
+scoped notation R' "⊗ᵣ'" ρ => baseChange R' ρ
+
+end Representation