Documentation

TauCeti.RepresentationTheory.Subrepresentation

The underlying module of a subrepresentation #

Mathlib's Subrepresentation API records how toSubmodule interacts with the lattice operations — Subrepresentation.toSubmodule_sup and Subrepresentation.toSubmodule_inf, both @[simp] and both true by rfl — but not how it interacts with the bounded-lattice structure, nor how it interacts with the order relations themselves, nor how it interacts with membership. This file adds the six missing counterparts, in the same shape. It also records that the representation action on a subrepresentation is the restriction of the original action, when an intertwining map is zero and when it is surjective in terms of the subrepresentation its range is, the inclusion of a subrepresentation as an intertwining map, that the group-algebra action on a subrepresentation coerces to the original action, the canonical equivalence between the module of the restricted representation and the corresponding submodule, and that a subrepresentation is minimal exactly when the A[G]-submodule it carries is simple.

They are stated at the typeclasses Subrepresentation itself asks for, so they apply wherever the abstraction does. The ⊥ and ⊤ lemmas let proofs about extreme subrepresentations avoid asserting the definitional unfolding of the BoundedOrder instance by hand; the ≤ and < lemmas move an order statement between the two lattices, which is what lets a submodule-level argument — a dimension count, say, or an orthogonal complement — settle a question about subrepresentations; and the membership lemma does the same for a single element, so that a carrier computed by a toSubmodule lemma answers a SetLike membership goal without unfolding the SetLike instance by hand. Representation.IntertwiningMap.eq_zero_iff_range_eq_bot and Representation.IntertwiningMap.surjective_iff_range_eq_top are the first consumers of the ⊥ and ⊤ lemmas, and belong here because ⊥ and ⊤ of Subrepresentation have no other API: they are LinearMap.range_eq_bot and LinearMap.range_eq_top moved up to the subrepresentation lattice, and Subrepresentation.subtype_eq_zero_iff and Subrepresentation.subtype_surjective_iff below are what they are proved for. In the same spirit, Subrepresentation.isSimpleModule_asSubmodule_iff moves the notion of an irreducible constituent across Subrepresentation.subrepresentationSubmoduleOrderIso, so that Mathlib's simple- and semisimple-module API applies to minimal subrepresentations; being about asSubmodule it asks for the coefficients to be a commutative ring, as Subrepresentation.asSubmodule and IsSimpleModule between them do. Subrepresentation.isCompl_toSubmodule is one more entry in the lattice dictionary, moving IsCompl across it, and stated with the rest of that dictionary at the typeclasses Subrepresentation itself asks for. Finally, Subrepresentation.equivProdOfIsCompl upgrades a complement to an equivalence of representations ρ ≃ ρ₁ × ρ₂: Submodule.prodEquivOfIsCompl supplies the linear isomorphism and each ρ g, being additive and preserving both summands, supplies the equivariance. Being about Submodule.prodEquivOfIsCompl, it asks for the coefficients to be a ring and the module to be a group, as that construction does.

Restriction along a surjective monoid homomorphism identifies the lattices of invariant submodules, keeping the underlying submodule in both directions. In particular it preserves irreducibility, as does restriction along a monoid isomorphism.

Main results #

source
@[simp]
theorem Subrepresentation.mem_toSubmodule {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {ρ' : Subrepresentation ρ} {v : W} :
v ∈ ρ'.toSubmodule ↔ v ∈ ρ'

A vector lies in the subspace a subrepresentation carries exactly when it lies in the subrepresentation. This is the SetLike instance of Subrepresentation, whose coercion is toSubmodule, stated as a lemma so that proofs need not unfold it.

source
@[simp]
theorem Subrepresentation.toSubmodule_bot {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} :
⊥.toSubmodule = ⊥

The bottom subrepresentation carries the bottom subspace.

source
@[simp]
theorem Subrepresentation.toSubmodule_top {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} :
⊤.toSubmodule = ⊤

The top subrepresentation carries the top subspace.

source
instance Subrepresentation.instNontrivial {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} [Nontrivial W] :
Nontrivial (Subrepresentation ρ)

The subrepresentation lattice of a nontrivial representation is nontrivial.

source
@[simp]
theorem Subrepresentation.toSubmodule_le_toSubmodule {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} :
ρ₁.toSubmodule ≤ ρ₂.toSubmodule ↔ ρ₁ ≤ ρ₂

One subrepresentation is contained in another exactly when the subspace it carries is.

source
@[simp]
theorem Subrepresentation.toSubmodule_lt_toSubmodule {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} :
ρ₁.toSubmodule < ρ₂.toSubmodule ↔ ρ₁ < ρ₂

One subrepresentation is strictly contained in another exactly when the subspace it carries is.

source
@[simp]
theorem Subrepresentation.isCompl_toSubmodule {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} :
IsCompl ρ₁.toSubmodule ρ₂.toSubmodule ↔ IsCompl ρ₁ ρ₂

Two subrepresentations are complementary exactly when the subspaces they carry are. This is the counterpart, for IsCompl, of Subrepresentation.toSubmodule_le_toSubmodule: it is what lets a splitting established in the submodule lattice -- by a dimension count, say, or by an explicit projection -- be read as a splitting of representations.

source
theorem Subrepresentation.toRepresentation_apply {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (S : Subrepresentation ρ) (g : G) :
S.toRepresentation g = (ρ g).restrict ⋯

The action on a subrepresentation is the restriction of the original action.

source
theorem Representation.IntertwiningMap.eq_zero_iff_range_eq_bot {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {V : Type u_4} [AddCommMonoid V] [Module A V] {τ : Representation A G V} (f : ρ.IntertwiningMap τ) :
f = 0 ↔ range ρ τ f = ⊥

An intertwining map is zero exactly when its range is the bottom subrepresentation.

source
theorem Representation.IntertwiningMap.surjective_iff_range_eq_top {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {V : Type u_4} [AddCommMonoid V] [Module A V] {τ : Representation A G V} (f : ρ.IntertwiningMap τ) :
Function.Surjective ⇑f ↔ range ρ τ f = ⊤

An intertwining map is surjective exactly when its range is the top subrepresentation.

source
def Subrepresentation.subtype {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
ρ'.toRepresentation.IntertwiningMap ρ

The inclusion of a subrepresentation, as an intertwining map: the analogue of Submodule.subtype, which is the linear map underlying it.

Equations
Instances For
    source
    @[simp]
    theorem Subrepresentation.coe_subtype {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    ⇑ρ'.subtype = Subtype.val

    The inclusion of a subrepresentation acts by the subtype coercion.

    source
    @[simp]
    theorem Subrepresentation.toLinearMap_subtype {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    ρ'.subtype.toLinearMap = ρ'.toSubmodule.subtype

    The linear map underlying the inclusion is the submodule subtype map.

    source
    @[simp]
    theorem Subrepresentation.range_subtype {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    Representation.IntertwiningMap.range ρ'.toRepresentation ρ ρ'.subtype = ρ'

    The range of the inclusion of a subrepresentation is that subrepresentation.

    source
    @[simp]
    theorem Subrepresentation.ker_subtype {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    Representation.IntertwiningMap.ker ρ'.toRepresentation ρ ρ'.subtype = ⊥

    The kernel of the inclusion of a subrepresentation is zero.

    source
    theorem Subrepresentation.subtype_injective {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    Function.Injective ⇑ρ'.subtype

    The inclusion of a subrepresentation is injective.

    source
    @[simp]
    theorem Subrepresentation.subtype_eq_zero_iff {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    ρ'.subtype = 0 ↔ ρ' = ⊥

    The inclusion of a subrepresentation is zero exactly when the subrepresentation is zero.

    source
    theorem Subrepresentation.subtype_surjective_iff {A : Type u_1} {G : Type u_2} {W : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
    Function.Surjective ⇑ρ'.subtype ↔ ρ' = ⊤

    The inclusion of a subrepresentation is surjective exactly when the subrepresentation is the whole representation.

    source
    @[simp]
    theorem Subrepresentation.coe_toRepresentation_asAlgebraHom_apply {k : Type u_4} {H : Type u_5} {V : Type u_6} [CommSemiring k] [Monoid H] [AddCommMonoid V] [Module k V] {σ : Representation k H V} (S : Subrepresentation σ) (a : MonoidAlgebra k H) (x : ↥S.toSubmodule) :
    ↑((S.toRepresentation.asAlgebraHom a) x) = (σ.asAlgebraHom a) ↑x

    The group-algebra action on a subrepresentation, coerced to the ambient module, is the original group-algebra action.

    source
    noncomputable def Subrepresentation.asModuleEquivAsSubmodule {A : Type u_4} {G : Type u_5} {W : Type u_6} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ) :
    σ.toRepresentation.asModule ≃ₗ[MonoidAlgebra A G] ↥σ.asSubmodule

    The module carried by a subrepresentation is canonically its associated submodule. The equivalence identifies both with the same invariant subset of the ambient representation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Subrepresentation.coe_asModuleEquivAsSubmodule_apply {A : Type u_4} {G : Type u_5} {W : Type u_6} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ) (x : σ.toRepresentation.asModule) :
      ↑(σ.asModuleEquivAsSubmodule x) = ↑(σ.toRepresentation.asModuleEquiv x)
      source
      @[simp]
      theorem Subrepresentation.coe_asModuleEquivAsSubmodule_symm_apply {A : Type u_4} {G : Type u_5} {W : Type u_6} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ) (x : ↥σ.asSubmodule) :
      ↑(σ.asModuleEquivAsSubmodule.symm x) = ρ.asModuleEquiv ↑x
      source
      @[simp]
      theorem Subrepresentation.isSimpleModule_asSubmodule_iff {A : Type u_4} {G : Type u_5} {W : Type u_6} [CommRing A] [Monoid G] [AddCommGroup W] [Module A W] {ρ : Representation A G W} {σ : Subrepresentation ρ} :
      IsSimpleModule (MonoidAlgebra A G) ↥σ.asSubmodule ↔ IsAtom σ

      A minimal subrepresentation is the same thing as a simple A[G]-submodule of the associated module: the dictionary between the two ways of saying "irreducible constituent". It is isSimpleModule_iff_isAtom read across Subrepresentation.subrepresentationSubmoduleOrderIso.

      source
      noncomputable def Subrepresentation.equivProdOfIsCompl {A : Type u_4} {G : Type u_5} {W : Type u_6} [Ring A] [Monoid G] [AddCommGroup W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} (h : IsCompl ρ₁ ρ₂) :
      ρ.Equiv (ρ₁.toRepresentation.prod ρ₂.toRepresentation)

      Complementary subrepresentations split the representation as a direct sum. Adding a vector of ρ₁ to one of ρ₂ is a linear isomorphism ρ₁ × ρ₂ ≃ W by Submodule.prodEquivOfIsCompl, and it is equivariant because every ρ g is additive and preserves each summand; so ρ is the product of the two representations the summands carry. This is the representation-theoretic content of a complement, of which Submodule.prodEquivOfIsCompl records only the linear part.

      Equations
      Instances For
        source
        @[simp]
        theorem Subrepresentation.equivProdOfIsCompl_apply {A : Type u_4} {G : Type u_5} {W : Type u_6} [Ring A] [Monoid G] [AddCommGroup W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} (h : IsCompl ρ₁ ρ₂) (v : W) :
        (equivProdOfIsCompl h) v = (ρ₁.toSubmodule.prodEquivOfIsCompl ρ₂.toSubmodule ⋯).symm v

        The splitting is the linear splitting Submodule.prodEquivOfIsCompl of the two carriers, read backwards: it sends a vector to the pair of its components along the complementary submodules.

        source
        @[simp]
        theorem Subrepresentation.equivProdOfIsCompl_symm_apply {A : Type u_4} {G : Type u_5} {W : Type u_6} [Ring A] [Monoid G] [AddCommGroup W] [Module A W] {ρ : Representation A G W} {ρ₁ ρ₂ : Subrepresentation ρ} (h : IsCompl ρ₁ ρ₂) (v : ↥ρ₁.toSubmodule × ↥ρ₂.toSubmodule) :
        (equivProdOfIsCompl h).symm v = ↑v.1 + ↑v.2

        The inverse of the splitting adds the two components back together.

        source
        def MonoidHom.resSubrepresentationOrderIso {k : Type u_1} [Semiring k] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {V : Type u_4} [AddCommMonoid V] [Module k V] (f : H →* K) (hf : Function.Surjective ⇑f) (ρ : Representation k K V) :
        Subrepresentation (comp ρ f) ≃o Subrepresentation ρ

        Restriction along a surjective monoid homomorphism identifies invariant subspaces: a subspace invariant under ρ ∘ f is invariant under ρ, because f is onto. Both directions keep the underlying submodule.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MonoidHom.resSubrepresentationOrderIso_apply_toSubmodule {k : Type u_1} [Semiring k] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {V : Type u_4} [AddCommMonoid V] [Module k V] (f : H →* K) (hf : Function.Surjective ⇑f) (ρ : Representation k K V) (S : Subrepresentation (comp ρ f)) :
          ((f.resSubrepresentationOrderIso hf ρ) S).toSubmodule = S.toSubmodule

          The forward invariant-subspace correspondence preserves the underlying submodule.

          source
          @[simp]
          theorem MonoidHom.resSubrepresentationOrderIso_symm_apply_toSubmodule {k : Type u_1} [Semiring k] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {V : Type u_4} [AddCommMonoid V] [Module k V] (f : H →* K) (hf : Function.Surjective ⇑f) (ρ : Representation k K V) (S : Subrepresentation ρ) :
          ((f.resSubrepresentationOrderIso hf ρ).symm S).toSubmodule = S.toSubmodule

          The inverse invariant-subspace correspondence preserves the underlying submodule.

          source
          @[simp]
          theorem MonoidHom.isIrreducible_comp_surjective_iff {k : Type u_1} [Field k] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {V : Type u_4} [AddCommGroup V] [Module k V] (f : H →* K) (hf : Function.Surjective ⇑f) (ρ : Representation k K V) :
          Representation.IsIrreducible (comp ρ f) ↔ ρ.IsIrreducible

          Restriction along a surjective monoid homomorphism preserves irreducibility: irreducibility is simplicity of the lattice of invariant subspaces, and MonoidHom.resSubrepresentationOrderIso identifies the two lattices.

          source
          @[simp]
          theorem MulEquiv.isIrreducible_comp_equiv_iff {k : Type u_1} [Field k] {H : Type u_2} {K : Type u_3} [Monoid H] [Monoid K] {V : Type u_4} [AddCommGroup V] [Module k V] (e : H ≃* K) (ρ : Representation k K V) :
          Representation.IsIrreducible (MonoidHom.comp ρ ↑e) ↔ ρ.IsIrreducible

          Restriction along a monoid isomorphism preserves irreducibility.