Lumenary.CategoricalRepresentationTheory

Formal library

• card_sumtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Decategorifying the disjoint union: `|A ⊔ B| = |A| + |B|`. This applies Mathlib's
  `Fintype.card_sum`. -/
  theorem card_sum (A B : Type*) [Fintype A] [Fintype B] :
      Fintype.card (A ⊕ B) = Fintype.card A + Fintype.card B :=
    Fintype.card_sum

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• card_prodtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Decategorifying the product: `|A × B| = |A| · |B|`. This applies Mathlib's
  `Fintype.card_prod`. -/
  theorem card_prod (A B : Type*) [Fintype A] [Fintype B] :
      Fintype.card (A × B) = Fintype.card A * Fintype.card B :=
    Fintype.card_prod A B

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• card_distribtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The distributive law `a(b + c) = ab + ac` is the shadow of a *bijection*
  `A × (B ⊔ C) ≃ (A × B) ⊔ (A × C)` (Mathlib's `Equiv.prodSumDistrib`). Categorified, an equation
  between numbers becomes an isomorphism between sets — extra information that the numbers forget
  (which bijection?). -/
  theorem card_distrib (A B C : Type*) [Fintype A] [Fintype B] [Fintype C] :
      Fintype.card (A × (B ⊕ C)) = Fintype.card (A × B) + Fintype.card (A × C) := by
    rw [Fintype.card_congr (Equiv.prodSumDistrib A B C), Fintype.card_sum]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• finrank_additivetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- Dimension is additive on short exact sequences `0 → A --f--> B --g--> C → 0`:
  `dim B = dim A + dim C`. Proof by rank–nullity for `g`: `dim B = dim im g + dim ker g`, where
  `im g = C` (surjectivity) and `ker g = im f ≅ A` (exactness and injectivity). This is exactly
  the relation `[B] = [A] + [C]` defining the Grothendieck group, so `dim` induces a homomorphism
  `K₀(vect_k) → ℤ` (in fact an isomorphism). -/
  theorem finrank_additive [FiniteDimensional k B] (f : A →ₗ[k] B) (g : B →ₗ[k] C)
      (hf : Function.Injective f) (hg : Function.Surjective g)
      (hexact : LinearMap.range f = LinearMap.ker g) :
      Module.finrank k B = Module.finrank k A + Module.finrank k C := by
    have hrn := LinearMap.finrank_range_add_finrank_ker g
    have hA : Module.finrank k (LinearMap.range f) = Module.finrank k A :=
      LinearMap.finrank_range_of_inj hf
    have hC : Module.finrank k (LinearMap.range g) = Module.finrank k C := by
      rw [LinearMap.range_eq_top.mpr hg, finrank_top]
    rw [← hexact, hA, hC] at hrn
    omega

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• euler_characteristic_two_termtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- For a two-term complex `V₁ --d--> V₀` of finite-dimensional spaces, the Euler
  characteristic of the complex equals that of its homology:
  `dim V₀ - dim V₁ = dim H₀ - dim H₁`, where `H₀ = coker d = V₀ / im d` and `H₁ = ker d`.
  Homology *categorifies* the Euler characteristic: it replaces a number by graded vector spaces
  whose alternating dimension recovers it. Proof: rank–nullity for `d`, and
  `dim (V₀ / im d) + dim im d = dim V₀`. -/
  theorem euler_characteristic_two_term [FiniteDimensional k V₁] [FiniteDimensional k V₀]
      (d : V₁ →ₗ[k] V₀) :
      (Module.finrank k V₀ : ℤ) - Module.finrank k V₁ =
        (Module.finrank k (V₀ ⧸ LinearMap.range d) : ℤ) - Module.finrank k (LinearMap.ker d) := by
    have h₁ := LinearMap.finrank_range_add_finrank_ker d
    have h₀ := Submodule.finrank_quotient_add_finrank (LinearMap.range d)
    omega

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• fdrep_symmetrictheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Finite-dimensional representations form a symmetric monoidal category under `⊗` (with `g`
  acting diagonally): the swap `β : V ⊗ W ≅ W ⊗ V` squares to the identity. This applies
  Mathlib's instance `SymmetricCategory (FDRep k G)` and the axiom `SymmetricCategory.symmetry`.
  (In a merely *braided* category, such as the representations of a quantum group, this fails.) -/
  theorem fdrep_symmetric (V W : FDRep k G) : (β_ V W).hom ≫ (β_ W V).hom = 𝟙 (V ⊗ W) :=
    SymmetricCategory.symmetry V W

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• fdrep_zigzagtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Every finite-dimensional representation `V` has a dual `Vᘁ` with coevaluation
  `η : 𝟙 → V ⊗ Vᘁ` and evaluation `ε : Vᘁ ⊗ V → 𝟙` satisfying the zig-zag identity
  `(V ◁ ε) ∘ α ∘ (η ▷ V) = ρ⁻¹ ∘ λ`: `FDRep k G` is rigid. This applies Mathlib's instance
  `RightRigidCategory (FDRep k G)` (inherited from `FGModuleCat k`) and
  `ExactPairing.evaluation_coevaluation`. -/
  theorem fdrep_zigzag (V : FDRep k G) :
      η_ V Vᘁ ▷ V ≫ (α_ _ _ _).hom ≫ V ◁ ε_ V Vᘁ = (λ_ V).hom ≫ (ρ_ V).inv :=
    ExactPairing.evaluation_coevaluation V Vᘁ

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• char_tensortheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Decategorifying `⊗`: the character of `V ⊗ W` is the product of the characters. Since
  characters are additive on direct sums and depend only on the isomorphism class (`char_iso`),
  the character is a ring homomorphism from the Grothendieck ring of `Rep(G)` to class
  functions. This applies Mathlib's `FDRep.char_tensor`. -/
  theorem char_tensor (V W : FDRep k G) : (V ⊗ W).character = V.character * W.character :=
    FDRep.char_tensor V W

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• char_isotheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Isomorphic representations have equal characters, so the character only sees the class
  `[V]` in the Grothendieck group. This applies Mathlib's `FDRep.char_iso`. -/
  theorem char_iso {V W : FDRep k G} (i : V ≅ W) : V.character = W.character :=
    FDRep.char_iso i

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• char_onetheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- Evaluating the character at the identity gives the dimension: `χ_V(1) = dim V`. So
  `dim : K₀(Rep G) → ℤ` is a ring homomorphism with positive values on non-zero
  representations. This applies Mathlib's `FDRep.char_one`. -/
  theorem char_one (V : FDRep k G) : V.character 1 = Module.finrank k V :=
    FDRep.char_one V

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

• fibonacci_no_integer_dimensiontheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- The Fibonacci fusion ring has basis `1, τ` with `τ ⊗ τ = 1 ⊕ τ`. A ring homomorphism to `ℤ`
  would send `τ` to an integer `n` with `n² = 1 + n`, and there is none. Since `dim` is a ring
  homomorphism `K₀(Rep G) → ℤ` (`char_one`, `char_tensor`), the Fibonacci fusion category is
  not `Rep(G)` for any finite group `G`. (Its Frobenius–Perron dimension is the golden ratio.) -/
  theorem fibonacci_no_integer_dimension : ¬ ∃ n : ℤ, n ^ 2 = 1 + n := by
    rintro ⟨n, hn⟩
    have h₁ : n ≤ 2 := by nlinarith
    have h₂ : -1 ≤ n := by nlinarith
    interval_cases n <;> omega

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalRepresentationTheory.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- No integer `n` satisfies `n² = 1 + n`, so the Fibonacci fusion rule `τ ⊗ τ = 1 ⊕ τ` has no
integer-valued dimension. Hint: bound `n` with `nlinarith`, then use `interval_cases n`. -/
theorem fibonacci_no_integer_dimension : ¬ ∃ n : ℤ, n ^ 2 = 1 + n := by
  sorry

/-- The Fibonacci fusion ring has basis `1, τ` with `τ ⊗ τ = 1 ⊕ τ`. A ring homomorphism to `ℤ`
would send `τ` to an integer `n` with `n² = 1 + n`, and there is none. Since `dim` is a ring
homomorphism `K₀(Rep G) → ℤ` (`char_one`, `char_tensor`), the Fibonacci fusion category is
not `Rep(G)` for any finite group `G`. (Its Frobenius–Perron dimension is the golden ratio.) -/
theorem fibonacci_no_integer_dimension : ¬ ∃ n : ℤ, n ^ 2 = 1 + n := by
  rintro ⟨n, hn⟩
  have h₁ : n ≤ 2 := by nlinarith
  have h₂ : -1 ≤ n := by nlinarith
  interval_cases n <;> omega