Conjugate representations

For a subgroup H of a group G and s : G, this file defines the conjugate of an H-representation as a representation of sHs⁻¹. The action is transported along the canonical isomorphism

sHs⁻¹ → H, x ↦ s⁻¹xs.

This is the representation occurring in the summands of the Mackey decomposition.

The conjugation convention itself, that MulAut.conj s • H is sHs⁻¹ and so that the membership proof conjRep needs is s⁻¹xs ∈ H, is pinned in TauCeti.Algebra.Group.Subgroup.Pointwise as TauCeti.mem_conj_smul, together with the laws TauCeti.conj_one_smul and TauCeti.conj_mul_smul making conjugation an action of G on the subgroups of G; the coherence below transports the representations along them.

The file also records the coherence making s ↦ {}^s(-) an action: conjugating by 1 does nothing and {}^{st} A = {}^s({}^t A). Neither statement is literally an equation between representations of one group, because {}^s({}^t A) is a representation of s(tHt⁻¹)s⁻¹ while {}^{st} A is a representation of (st)H(st)⁻¹; the two subgroups are equal, and the coherence is stated after transporting along that equality with MulEquiv.subgroupCongr and Rep.res. Both halves are proved as equalities of functors; the statements about a single representation are their evaluations.

For a normal subgroup N the conjugated subgroup is N itself, so no transport is needed: conjugation by g is an endofunctor of Rep k N, indeed an autoequivalence, and the coherence makes g ↦ conjNormalRep g a MulAction of G on Rep k N. This is the action of G on Rep k N that Clifford theory runs on. Because conjugation is a functor, it descends along CategoryTheory.Functor.mapSkeleton to isomorphism classes, giving the action of G on CategoryTheory.Skeleton (FDRep k N) whose stabilizers are the inertia groups (TauCeti.RepresentationTheory.Induction.Inertia); those stabilizers are not MulAction.stabilizer G A, which asks for {}^g A = A on the nose. Conjugation does preserve irreducibility (TauCeti.isIrreducible_conjRep_iff, TauCeti.isIrreducible_conjFDRep_iff), since it identifies the invariant subspaces; the restriction of the action on isomorphism classes to the irreducible ones is not carved out here.

Main definitions

• TauCeti.conjSubgroupEquiv: the canonical isomorphism from sHs⁻¹ to H.
• TauCeti.conjRepFunctor, TauCeti.conjFDRepFunctor: conjugation as a functor between representation categories, with TauCeti.conjRepEquiv and TauCeti.conjFDRepEquiv the equivalences Rep k H ≌ Rep k (sHs⁻¹) and FDRep k H ≌ FDRep k (sHs⁻¹) they underlie.
• TauCeti.conjRep: the conjugate of a representation.
• TauCeti.conjRepSubrepresentationOrderIso: the invariant-subspace correspondence under conjugation.
• TauCeti.conjFDRep: the finite-dimensional version.
• TauCeti.conjNormalRepFunctor, TauCeti.conjNormalFDRepFunctor: for a normal subgroup, conjugation as an endofunctor, with TauCeti.conjNormalRepEquiv and TauCeti.conjNormalFDRepEquiv the autoequivalences they underlie.
• TauCeti.conjNormalRep, TauCeti.conjNormalFDRep: conjugation of a representation of a normal subgroup, again a representation of that subgroup; these are the MulAction of G on Rep k N and on FDRep k N.
• TauCeti.conjNormalFDRepIso: conjugating by an element of N itself is an inner twist, so it gives an isomorphic representation.
• TauCeti.conjNormalFDRepSkeletonSMul, TauCeti.conjNormalFDRepSkeletonMulAction: conjugation acting on isomorphism classes of finite-dimensional representations of N.

Main statements

• TauCeti.conjRepFunctor_one, TauCeti.conjRepFunctor_mul and their FDRep counterparts: the coherence of conjugation, as equalities of functors, up to the identification of the conjugated subgroups; TauCeti.conjRep_one, TauCeti.conjRep_mul evaluate them at a representation.
• TauCeti.conjNormalRep_one, TauCeti.conjNormalRep_mul and their FDRep counterparts: for a normal subgroup that coherence becomes a genuine left action of G, recorded as MulAction instances.
• TauCeti.Representation.apply_conjNormal_inv: the basic intertwining identity between an ambient representation operator and the action of a normal subgroup.
• Representation.apply_conjNormal_coe: its inner counterpart for a representation of the normal subgroup itself.
• TauCeti.res_conjRep, TauCeti.res_conjFDRep: the normal-subgroup conjugation is the general conjugate representation, read through MulAut.conj g • N = N.
• TauCeti.isIrreducible_conjRep_iff, TauCeti.isIrreducible_conjFDRep_iff: conjugation preserves irreducibility, because it identifies the invariant subspaces.

def TauCeti.conjSubgroupEquiv {G : Type v} [Group G] (s : G) (H : Subgroup G) : ↥(MulAut.conj s • H) ≃* ↥H

The canonical multiplicative equivalence sHs⁻¹ ≃* H, given by x ↦ s⁻¹xs.

Equations

• TauCeti.conjSubgroupEquiv s H = (Subgroup.equivSMul (MulAut.conj s) H).symm

@[simp]

theorem TauCeti.coe_conjSubgroupEquiv_apply {G : Type v} [Group G] (s : G) (H : Subgroup G) (x : ↥(MulAut.conj s • H)) : ↑((conjSubgroupEquiv s H) x) = s⁻¹ * ↑x * s

@[simp]

theorem TauCeti.coe_conjSubgroupEquiv_symm_apply {G : Type v} [Group G] (s : G) (H : Subgroup G) (x : ↥H) : ↑((conjSubgroupEquiv s H).symm x) = s * ↑x * s⁻¹

def TauCeti.conjRepFunctor {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) : CategoryTheory.Functor (Rep k ↥H) (Rep k ↥(MulAut.conj s • H))

Conjugating representations by s is restriction along the isomorphism sHs⁻¹ ≃* H.

Equations

• TauCeti.conjRepFunctor s H = Rep.resFunctor (TauCeti.conjSubgroupEquiv s H).toMonoidHom

def TauCeti.conjRep {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) : Rep k ↥(MulAut.conj s • H)

The conjugate representation {}^s A of sHs⁻¹.

Equations

• TauCeti.conjRep s A = (TauCeti.conjRepFunctor s H).obj A

theorem TauCeti.res_obj_eq_conjRep {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) (A : Rep k ↥H) : Rep.res (↑(conjSubgroupEquiv s H)) A = conjRep s A

Restriction along conjSubgroupEquiv sends A to conjRep s A. The Rep mirror of res_obj_eq_conjFDRep.

@[simp]

theorem TauCeti.conjRep_V {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) : ↑(conjRep s A) = ↑A

Conjugation preserves the underlying module of a representation.

theorem TauCeti.conjRepFunctor_map_hom_toLinearMap {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} {A B : Rep k ↥H} (f : A ⟶ B) : (Rep.Hom.hom ((conjRepFunctor s H).map f)).toLinearMap ≍ (Rep.Hom.hom f).toLinearMap

Conjugation preserves the underlying linear map of a representation morphism.

theorem TauCeti.conjRep_ρ {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) (x : ↥(MulAut.conj s • H)) : (conjRep s A).ρ x ≍ A.ρ ((conjSubgroupEquiv s H) x)

The conjugate action, as a heterogeneous equality: conjRep is opaque, so (conjRep s A).V and A.V are equal only via conjRep_V, not definitionally.

theorem TauCeti.conjRep_ρ_apply {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) (x : ↥(MulAut.conj s • H)) (v : ↑A) : cast ⋯ (((conjRep s A).ρ x) (cast ⋯ v)) = (A.ρ ((conjSubgroupEquiv s H) x)) v

The conjugate action on elements, transported along conjRep_V.

theorem TauCeti.conjRep_ρ_mk {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) (x : ↥(MulAut.conj s • H)) : (conjRep s A).ρ x ≍ A.ρ ⟨s⁻¹ * ↑x * s, ⋯⟩

The action of the conjugate representation, written directly in the ambient group.

def TauCeti.conjRepSubrepresentationOrderIso {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) : Subrepresentation (conjRep s A).ρ ≃o Subrepresentation A.ρ

Conjugation identifies the invariant subspaces of a representation with those of its conjugate.

Equations

• TauCeti.conjRepSubrepresentationOrderIso s A = id ((TauCeti.conjSubgroupEquiv s H).toMonoidHom.resSubrepresentationOrderIso ⋯ A.ρ)

@[simp]

theorem TauCeti.conjRepSubrepresentationOrderIso_apply_toSubmodule {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) (S : Subrepresentation (conjRep s A).ρ) : ((conjRepSubrepresentationOrderIso s A) S).toSubmodule ≍ S.toSubmodule

The forward invariant-subspace correspondence preserves the underlying submodule.

@[simp]

theorem TauCeti.conjRepSubrepresentationOrderIso_symm_apply_toSubmodule {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) {H : Subgroup G} (A : Rep k ↥H) (S : Subrepresentation A.ρ) : ((conjRepSubrepresentationOrderIso s A).symm S).toSubmodule ≍ S.toSubmodule

The inverse invariant-subspace correspondence preserves the underlying submodule.

@[simp]

theorem TauCeti.isIrreducible_conjRep_iff {k : Type u} {G : Type v} [Group G] [Field k] (s : G) {H : Subgroup G} (A : Rep k ↥H) : (conjRep s A).ρ.IsIrreducible ↔ A.ρ.IsIrreducible

A conjugate representation is irreducible exactly when the original representation is.

theorem TauCeti.conjRepFunctor_one {k : Type u} {G : Type v} [Group G] [Semiring k] (H : Subgroup G) : conjRepFunctor 1 H = Rep.resFunctor (MulEquiv.subgroupCongr ⋯).toMonoidHom

Conjugating by 1 does nothing, once 1 · H · 1⁻¹ is identified with H: an equality of functors, of which conjRep_one is the evaluation at a representation.

theorem TauCeti.conjRepFunctor_mul {k : Type u} {G : Type v} [Group G] [Semiring k] (s t : G) (H : Subgroup G) : conjRepFunctor (s * t) H = (conjRepFunctor t H).comp ((conjRepFunctor s (MulAut.conj t • H)).comp (Rep.resFunctor (MulEquiv.subgroupCongr ⋯).toMonoidHom))

Cocycle coherence for conjugation, at the level of functors: {}^{st}(-) = {}^s({}^t(-)), once (st)H(st)⁻¹ is identified with s(tHt⁻¹)s⁻¹. Being an equality of functors this also pins down the behaviour on morphisms, which the evaluation conjRep_mul does not see.

Together with conjRepFunctor_one this is what makes s ↦ {}^s(-) an action of G; both Mackey theory (where a double-coset representative may be replaced by another) and Clifford theory consume it.

theorem TauCeti.conjRep_one {k : Type u} {G : Type v} [Group G] [Semiring k] {H : Subgroup G} (A : Rep k ↥H) : conjRep 1 A = Rep.res (MulEquiv.subgroupCongr ⋯).toMonoidHom A

Conjugating by 1 does nothing, once 1 · H · 1⁻¹ is identified with H.

theorem TauCeti.conjRep_mul {k : Type u} {G : Type v} [Group G] [Semiring k] (s t : G) {H : Subgroup G} (A : Rep k ↥H) : conjRep (s * t) A = Rep.res (MulEquiv.subgroupCongr ⋯).toMonoidHom (conjRep s (conjRep t A))

Cocycle coherence for conjugation: {}^{st} A = {}^s({}^t A), once (st)H(st)⁻¹ is identified with s(tHt⁻¹)s⁻¹. The evaluation of conjRepFunctor_mul at A.

def TauCeti.conjRepEquiv {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) : Rep k ↥H ≌ Rep k ↥(MulAut.conj s • H)

Conjugation is an equivalence of categories Rep k H ≌ Rep k (sHs⁻¹): it is restriction along the isomorphism conjSubgroupEquiv s H, and MulEquiv.resFunctorEquiv makes any such restriction an equivalence. Its inverse is conjugation by s⁻¹, read through s⁻¹(sHs⁻¹)s = H (conjRepEquiv_inverse_eq_conjRepFunctor).

conjNormalRepEquiv is the normal-subgroup form, where source and target coincide, so that the equivalence is an autoequivalence and the coherence below becomes an action.

Equations

• TauCeti.conjRepEquiv s H = (TauCeti.conjSubgroupEquiv s H).resFunctorEquiv

@[simp]

theorem TauCeti.conjRepEquiv_functor {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) : (conjRepEquiv s H).functor = conjRepFunctor s H

@[simp]

theorem TauCeti.conjRepEquiv_inverse {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) : (conjRepEquiv s H).inverse = Rep.resFunctor (conjSubgroupEquiv s H).symm.toMonoidHom

theorem TauCeti.conjRepEquiv_inverse_eq_conjRepFunctor {k : Type u} {G : Type v} [Group G] [Semiring k] (s : G) (H : Subgroup G) : (conjRepEquiv s H).inverse = (conjRepFunctor s⁻¹ (MulAut.conj s • H)).comp (Rep.resFunctor (MulEquiv.subgroupCongr ⋯).toMonoidHom)

The inverse of the conjugation equivalence is conjugation by s⁻¹, once s⁻¹(sHs⁻¹)s is identified with H.

def TauCeti.conjFDRepFunctor {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) : CategoryTheory.Functor (FDRep k ↥H) (FDRep k ↥(MulAut.conj s • H))

Conjugating finite-dimensional representations by s is restriction along the isomorphism sHs⁻¹ ≃* H. The FDRep mirror of conjRepFunctor: FDRep k H is by definition Action (FGModuleCat k) H, so the restriction functor is Mathlib's Action.res.

Equations

• TauCeti.conjFDRepFunctor s H = Action.res (FGModuleCat k) (TauCeti.conjSubgroupEquiv s H).toMonoidHom

def TauCeti.conjFDRep {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) : FDRep k ↥(MulAut.conj s • H)

The conjugate of a finite-dimensional representation.

Equations

• TauCeti.conjFDRep s A = (TauCeti.conjFDRepFunctor s H).obj A

@[simp]

theorem TauCeti.res_obj_eq_conjFDRep {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) (A : FDRep k ↥H) : (Action.res (FGModuleCat k) ↑(conjSubgroupEquiv s H)).obj A = conjFDRep s A

Restriction along conjSubgroupEquiv sends A to conjFDRep s A.

@[simp]

theorem TauCeti.conjFDRep_V {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) : (conjFDRep s A).V = A.V

Conjugation preserves the underlying module of a finite-dimensional representation.

theorem TauCeti.conjFDRepFunctor_one {k : Type u} {G : Type v} [Group G] [Ring k] (H : Subgroup G) : conjFDRepFunctor 1 H = Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom

Conjugating by 1 does nothing, as an equality of functors. The FDRep mirror of conjRepFunctor_one.

theorem TauCeti.conjFDRepFunctor_mul {k : Type u} {G : Type v} [Group G] [Ring k] (s t : G) (H : Subgroup G) : conjFDRepFunctor (s * t) H = (conjFDRepFunctor t H).comp ((conjFDRepFunctor s (MulAut.conj t • H)).comp (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom))

Cocycle coherence for finite-dimensional representations, at the level of functors. The FDRep mirror of conjRepFunctor_mul, and the form in which the character computations of Mackey and Clifford theory use it.

theorem TauCeti.conjFDRep_one {k : Type u} {G : Type v} [Group G] [Ring k] {H : Subgroup G} (A : FDRep k ↥H) : conjFDRep 1 A = (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom).obj A

Conjugating a finite-dimensional representation by 1 does nothing, once 1 · H · 1⁻¹ is identified with H. The FDRep mirror of conjRep_one.

theorem TauCeti.conjFDRep_mul {k : Type u} {G : Type v} [Group G] [Ring k] (s t : G) {H : Subgroup G} (A : FDRep k ↥H) : conjFDRep (s * t) A = (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom).obj (conjFDRep s (conjFDRep t A))

Cocycle coherence for finite-dimensional representations: {}^{st} A = {}^s({}^t A), once (st)H(st)⁻¹ is identified with s(tHt⁻¹)s⁻¹. The evaluation of conjFDRepFunctor_mul at A.

def TauCeti.conjFDRepEquiv {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) : FDRep k ↥H ≌ FDRep k ↥(MulAut.conj s • H)

Conjugation is an equivalence FDRep k H ≌ FDRep k (sHs⁻¹). The FDRep mirror of conjRepEquiv; here FDRep k H is Action (FGModuleCat k) H, so this is Mathlib's Action.resEquiv for conjSubgroupEquiv s H.

Equations

• TauCeti.conjFDRepEquiv s H = Action.resEquiv (FGModuleCat k) (TauCeti.conjSubgroupEquiv s H)

@[simp]

theorem TauCeti.conjFDRepEquiv_functor {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) : (conjFDRepEquiv s H).functor = conjFDRepFunctor s H

@[simp]

theorem TauCeti.conjFDRepEquiv_inverse {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) : (conjFDRepEquiv s H).inverse = Action.res (FGModuleCat k) (conjSubgroupEquiv s H).symm.toMonoidHom

theorem TauCeti.conjFDRepEquiv_inverse_eq_conjFDRepFunctor {k : Type u} {G : Type v} [Group G] [Ring k] (s : G) (H : Subgroup G) : (conjFDRepEquiv s H).inverse = (conjFDRepFunctor s⁻¹ (MulAut.conj s • H)).comp (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom)

The inverse of the conjugation equivalence is conjugation by s⁻¹, once s⁻¹(sHs⁻¹)s is identified with H. The FDRep mirror of conjRepEquiv_inverse_eq_conjRepFunctor.

The conjugate action on a finite-dimensional representation

Mathlib develops FDRep.ρ and the coercion of an FDRep to a type only over a commutative ring, so the statements about the conjugate action and the dimension ask for [CommRing k], while the definitions and the coherence above need only [Ring k].

theorem TauCeti.conjFDRep_ρ {k : Type u} {G : Type v} [Group G] [CommRing k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) (x : ↥(MulAut.conj s • H)) : (conjFDRep s A).ρ x ≍ A.ρ ((conjSubgroupEquiv s H) x)

The conjugate finite-dimensional action, as a heterogeneous equality.

theorem TauCeti.conjFDRep_ρ_cast {k : Type u} {G : Type v} [Group G] [CommRing k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) (x : ↥(MulAut.conj s • H)) : cast ⋯ ((conjFDRep s A).ρ x) = A.ρ ((conjSubgroupEquiv s H) x)

The conjugate action, transported along conjFDRep_V.

@[simp]

theorem TauCeti.finrank_conjFDRep {k : Type u} {G : Type v} [Group G] [CommRing k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) : Module.finrank k ↑(conjFDRep s A).V = Module.finrank k ↑A.V

Conjugation preserves the dimension (finrank) of a finite-dimensional representation.

@[simp]

theorem TauCeti.isIrreducible_conjFDRep_iff {k : Type u} {G : Type v} [Group G] [Field k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) : Representation.IsIrreducible (conjFDRep s A).ρ ↔ Representation.IsIrreducible A.ρ

A conjugate finite-dimensional representation is irreducible exactly when the original representation is.

@[simp]

theorem TauCeti.char_conjFDRep {k : Type u} {G : Type v} [Group G] [Field k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) (x : ↥(MulAut.conj s • H)) : (conjFDRep s A).character x = A.character ((conjSubgroupEquiv s H) x)

The character of a conjugate representation is evaluated through conjSubgroupEquiv.

theorem TauCeti.char_conjFDRep_mk {k : Type u} {G : Type v} [Group G] [Field k] (s : G) {H : Subgroup G} (A : FDRep k ↥H) (x : ↥(MulAut.conj s • H)) : (conjFDRep s A).character x = A.character ⟨s⁻¹ * ↑x * s, ⋯⟩

The conjugate-character formula ({}^s χ)(x) = χ(s⁻¹xs).

Conjugation on a normal subgroup

For N ◁ G the conjugated subgroup MulAut.conj g • N is N itself (Subgroup.Normal.conj_smul_eq_self), so conjugation does not move the group it is a representation of: it is an endofunctor of Rep k N, in fact an autoequivalence, and the coherence of the previous sections becomes a genuine left action of G on Rep k N, recorded as a MulAction instance. This is the action of G on Rep k N that Clifford theory runs on.

theorem TauCeti.Representation.apply_conjNormal_inv {V : Type u_1} {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (n : ↥N) (v : V) : (ρ g) ((ρ ↑((MulAut.conjNormal g⁻¹) n)) v) = (ρ ↑n) ((ρ g) v)

Acting by g and then by n ∈ N is the same as acting by the conjugate g⁻¹ n g and then by g. This conjugation identity underlies both translated normal-subgroup subrepresentations and the transport of normal-subgroup weight spaces.

def TauCeti.conjNormalRepFunctor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) : CategoryTheory.Functor (Rep k ↥N) (Rep k ↥N)

Conjugation by g as an endofunctor of Rep k N: for a normal subgroup the conjugated subgroup is N again, so conjRepFunctor becomes an endofunctor, namely restriction along Mathlib's MulAut.conjNormal g⁻¹. It is an autoequivalence; see conjNormalRepEquiv.

@[expose] because the whole point of the normal-subgroup case is that the carrier is A.V on the nose, which is what lets conjNormalRep_ρ and its consequences be plain equalities rather than the heterogeneous ones conjRep_ρ is forced into.

Equations

• TauCeti.conjNormalRepFunctor g = Rep.resFunctor (MulEquiv.toMonoidHom (MulAut.conjNormal g⁻¹))

def TauCeti.conjNormalRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) : Rep k ↥N

The conjugate {}^g A of a representation of a normal subgroup N, again a representation of N: the element x : N acts by A.ρ (g⁻¹ x g).

This is conjRep with the conjugated subgroup identified with N, as res_conjRep records; the conjugating automorphism is Mathlib's MulAut.conjNormal g⁻¹.

Equations

• TauCeti.conjNormalRep g A = (TauCeti.conjNormalRepFunctor g).obj A

theorem TauCeti.conjNormalRep_V {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) : ↑(conjNormalRep g A) = ↑A

Conjugation on a normal subgroup preserves the underlying module. Not a simp lemma: it is rfl, and as a rewrite it fires inside the type of the left-hand side of conjNormalRep_ρ.

@[simp]

theorem TauCeti.conjNormalRep_ρ {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) (x : ↥N) : (conjNormalRep g A).ρ x = A.ρ ((MulAut.conjNormal g⁻¹) x)

The conjugate action on a normal subgroup. Unlike conjRep_ρ this is an honest equality: the two representations are representations of the same group, on the same module.

theorem TauCeti.conjNormalRep_ρ_mk {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) (x : ↥N) : (conjNormalRep g A).ρ x = A.ρ ⟨g⁻¹ * ↑x * g, ⋯⟩

The conjugate action on a normal subgroup, written in the ambient group.

theorem TauCeti.res_conjRepFunctor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) : (conjRepFunctor g N).comp (Rep.resFunctor (MulEquiv.subgroupCongr ⋯).toMonoidHom) = conjNormalRepFunctor g

On a normal subgroup, the conjugation functor conjRepFunctor, read through the identification gNg⁻¹ = N, is conjNormalRepFunctor.

theorem TauCeti.res_conjRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) : Rep.res (MulEquiv.subgroupCongr ⋯).toMonoidHom (conjRep g A) = conjNormalRep g A

On a normal subgroup, conjNormalRep is the general conjugate representation conjRep, read through the identification gNg⁻¹ = N.

theorem TauCeti.conjNormalRepFunctor_one {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] : conjNormalRepFunctor 1 = CategoryTheory.Functor.id (Rep k ↥N)

Conjugating by 1 is the identity endofunctor.

theorem TauCeti.conjNormalRepFunctor_mul {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (s t : G) : conjNormalRepFunctor (s * t) = (conjNormalRepFunctor t).comp (conjNormalRepFunctor s)

Conjugation is a left action, as an equality of endofunctors: {}^{st}(-) = {}^s({}^t(-)).

@[simp]

theorem TauCeti.conjNormalRep_one {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (A : Rep k ↥N) : conjNormalRep 1 A = A

Conjugating by 1 is the identity.

@[simp]

theorem TauCeti.conjNormalRep_mul {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (s t : G) (A : Rep k ↥N) : conjNormalRep (s * t) A = conjNormalRep s (conjNormalRep t A)

Conjugation is a left action: {}^{st} A = {}^s({}^t A).

def TauCeti.conjNormalRepEquiv {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) : Rep k ↥N ≌ Rep k ↥N

Conjugation by g is an autoequivalence of Rep k N, with inverse conjugation by g⁻¹: the autoequivalence used in Clifford theory. Conjugation on a normal subgroup is restriction along the automorphism MulAut.conjNormal g⁻¹, so this is MulEquiv.resFunctorEquiv for that automorphism, exactly as conjNormalFDRepEquiv is Mathlib's Action.resEquiv for it.

The body is sealed; conjNormalRepEquiv_functor and conjNormalRepEquiv_inverse are the interface identifying it with conjugation.

Equations

• TauCeti.conjNormalRepEquiv g = MulEquiv.resFunctorEquiv (MulAut.conjNormal g⁻¹)

@[simp]

theorem TauCeti.conjNormalRepEquiv_functor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) : (conjNormalRepEquiv g).functor = conjNormalRepFunctor g

@[simp]

theorem TauCeti.conjNormalRepEquiv_inverse {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) : (conjNormalRepEquiv g).inverse = conjNormalRepFunctor g⁻¹

@[instance_reducible]

instance TauCeti.conjNormalRepMulAction {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] : MulAction G (Rep k ↥N)

Conjugation is a left action of G on Rep k N: g • A is conjNormalRep g A. Clifford theory's inertia group of A is the stabilizer of the isomorphism class of A, {g | {}^g A ≅ A}, rather than MulAction.stabilizer G A, which asks for {}^g A = A on the nose; the induced action on isomorphism classes is not constructed here.

Equations

• TauCeti.conjNormalRepMulAction = { smul := TauCeti.conjNormalRep, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.smul_eq_conjNormalRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Semiring k] (g : G) (A : Rep k ↥N) : g • A = conjNormalRep g A

def TauCeti.conjNormalFDRepFunctor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) : CategoryTheory.Functor (FDRep k ↥N) (FDRep k ↥N)

Conjugation by g as an endofunctor of FDRep k N. The FDRep mirror of conjNormalRepFunctor: FDRep k N is by definition Action (FGModuleCat k) N, so this is Mathlib's Action.res along the conjugating automorphism, and the underlying module of an object is unchanged on the nose.

Equations

• TauCeti.conjNormalFDRepFunctor g = Action.res (FGModuleCat k) (MulEquiv.toMonoidHom (MulAut.conjNormal g⁻¹))

def TauCeti.conjNormalFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : FDRep k ↥N

The conjugate {}^g A of a finite-dimensional representation of a normal subgroup, again a finite-dimensional representation of that subgroup.

Equations

• TauCeti.conjNormalFDRep g A = (TauCeti.conjNormalFDRepFunctor g).obj A

theorem TauCeti.conjNormalFDRep_V {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : (conjNormalFDRep g A).V = A.V

Conjugation on a normal subgroup preserves the underlying module. Not a simp lemma, for the same reason as conjNormalRep_V.

theorem TauCeti.res_conjFDRepFunctor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) : (conjFDRepFunctor g N).comp (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom) = conjNormalFDRepFunctor g

On a normal subgroup, the conjugation functor conjFDRepFunctor, read through the identification gNg⁻¹ = N, is conjNormalFDRepFunctor. The FDRep mirror of res_conjRepFunctor.

theorem TauCeti.res_conjFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : (Action.res (FGModuleCat k) (MulEquiv.subgroupCongr ⋯).toMonoidHom).obj (conjFDRep g A) = conjNormalFDRep g A

On a normal subgroup, conjNormalFDRep is conjFDRep read through gNg⁻¹ = N.

theorem TauCeti.conjNormalFDRepFunctor_one {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] : conjNormalFDRepFunctor 1 = CategoryTheory.Functor.id (FDRep k ↥N)

Conjugating by 1 is the identity endofunctor. The FDRep mirror of conjNormalRepFunctor_one.

theorem TauCeti.conjNormalFDRepFunctor_mul {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (s t : G) : conjNormalFDRepFunctor (s * t) = (conjNormalFDRepFunctor t).comp (conjNormalFDRepFunctor s)

Conjugation is a left action, as an equality of endofunctors. The FDRep mirror of conjNormalRepFunctor_mul.

@[simp]

theorem TauCeti.conjNormalFDRep_one {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) : conjNormalFDRep 1 A = A

Conjugating by 1 is the identity.

@[simp]

theorem TauCeti.conjNormalFDRep_mul {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (s t : G) (A : FDRep k ↥N) : conjNormalFDRep (s * t) A = conjNormalFDRep s (conjNormalFDRep t A)

Conjugation is a left action: {}^{st} A = {}^s({}^t A).

def TauCeti.conjNormalFDRepEquiv {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) : FDRep k ↥N ≌ FDRep k ↥N

Conjugation by g is an autoequivalence of FDRep k N, with inverse conjugation by g⁻¹: Mathlib's Action.resEquiv for the automorphism MulAut.conjNormal g⁻¹ of N.

The body is sealed, as for conjNormalRepEquiv; conjNormalFDRepEquiv_functor and conjNormalFDRepEquiv_inverse are the interface identifying it with conjugation.

Equations

• TauCeti.conjNormalFDRepEquiv g = Action.resEquiv (FGModuleCat k) (MulAut.conjNormal g⁻¹)

@[simp]

theorem TauCeti.conjNormalFDRepEquiv_functor {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) : (conjNormalFDRepEquiv g).functor = conjNormalFDRepFunctor g

@[simp]

theorem TauCeti.conjNormalFDRepEquiv_inverse {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) : (conjNormalFDRepEquiv g).inverse = conjNormalFDRepFunctor g⁻¹

@[instance_reducible]

instance TauCeti.conjNormalFDRepMulAction {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] : MulAction G (FDRep k ↥N)

Conjugation is a left action of G on FDRep k N. The FDRep mirror of the MulAction on Rep k N.

Equations

• TauCeti.conjNormalFDRepMulAction = { smul := TauCeti.conjNormalFDRep, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.smul_eq_conjNormalFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : g • A = conjNormalFDRep g A

def TauCeti.conjNormalFDRepIso {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) (n : ↥N) : conjNormalFDRep (↑n) A ≅ A

Conjugating a representation of a normal subgroup N by an element n of N itself does not change its isomorphism class: the action of n is an isomorphism {}^n A ≅ A.

The intertwining property is the computation n · (n⁻¹xn) = xn in N.

Equations

• TauCeti.conjNormalFDRepIso A n = Action.mkIso ((Action.ρAut A) n) ⋯

@[simp]

theorem TauCeti.conjNormalFDRepIso_hom_hom {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (A : FDRep k ↥N) (n : ↥N) : (conjNormalFDRepIso A n).hom.hom = A.ρ n

The isomorphism {}^n A ≅ A for n : N is the action of n.

@[instance_reducible]

noncomputable instance TauCeti.conjNormalFDRepSkeletonSMul {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] : SMul G (CategoryTheory.Skeleton (FDRep k ↥N))

Conjugation acts on the isomorphism classes of finite-dimensional representations of N: the descent of the conjugation functor to the skeleton is Mathlib's CategoryTheory.Functor.mapSkeleton.

Equations

• TauCeti.conjNormalFDRepSkeletonSMul = { smul := fun (g : G) => (TauCeti.conjNormalFDRepFunctor g).mapSkeleton.obj }

@[simp]

theorem TauCeti.smul_toSkeleton {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] (g : G) (A : FDRep k ↥N) : g • CategoryTheory.toSkeleton A = CategoryTheory.toSkeleton (conjNormalFDRep g A)

The action on isomorphism classes is induced by the action on representations.

@[instance_reducible]

noncomputable instance TauCeti.conjNormalFDRepSkeletonMulAction {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Ring k] : MulAction G (CategoryTheory.Skeleton (FDRep k ↥N))

Conjugation on isomorphism classes is an action, because conjugation is one (conjNormalFDRep_one, conjNormalFDRep_mul); every class is toSkeleton of a representative, so smul_toSkeleton reduces both laws to their counterparts on representations.

This is the action whose stabilizers are the inertia groups (TauCeti.inertia).

Equations

• TauCeti.conjNormalFDRepSkeletonMulAction = { toSMul := TauCeti.conjNormalFDRepSkeletonSMul, mul_smul := ⋯, one_smul := ⋯ }

The conjugate action on a normal subgroup, in finite dimensions

As in the general case, FDRep.ρ and the coercion of an FDRep to a type are Mathlib API over a commutative ring, so these statements ask for [CommRing k].

@[simp]

theorem TauCeti.conjNormalFDRep_ρ {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [CommRing k] (g : G) (A : FDRep k ↥N) (x : ↥N) : (conjNormalFDRep g A).ρ x = A.ρ ((MulAut.conjNormal g⁻¹) x)

The conjugate finite-dimensional action on a normal subgroup, as an honest equality.

theorem TauCeti.conjNormalFDRep_ρ_mk {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [CommRing k] (g : G) (A : FDRep k ↥N) (x : ↥N) : (conjNormalFDRep g A).ρ x = A.ρ ⟨g⁻¹ * ↑x * g, ⋯⟩

The conjugate finite-dimensional action, written in the ambient group.

@[simp]

theorem TauCeti.finrank_conjNormalFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [CommRing k] (g : G) (A : FDRep k ↥N) : Module.finrank k ↑(conjNormalFDRep g A).V = Module.finrank k ↑A.V

Conjugation on a normal subgroup preserves the dimension.

@[simp]

theorem TauCeti.char_conjNormalFDRep {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Field k] (g : G) (A : FDRep k ↥N) (x : ↥N) : (conjNormalFDRep g A).character x = A.character ((MulAut.conjNormal g⁻¹) x)

The character of the conjugate of a representation of a normal subgroup.

theorem TauCeti.char_conjNormalFDRep_mk {k : Type u} {G : Type v} [Group G] {N : Subgroup G} [hN : N.Normal] [Field k] (g : G) (A : FDRep k ↥N) (x : ↥N) : (conjNormalFDRep g A).character x = A.character ⟨g⁻¹ * ↑x * g, ⋯⟩

The conjugate-character formula on a normal subgroup: ({}^g χ)(x) = χ(g⁻¹xg).

theorem Representation.apply_conjNormal_coe {k : Type u} {G : Type v} {V : Type w} [Group G] [Semiring k] [AddCommMonoid V] [Module k V] {N : Subgroup G} [N.Normal] (σ : Representation k (↥N) V) (m n : ↥N) (v : V) : (σ m) ((σ n) v) = (σ ((MulAut.conjNormal ↑m) n)) ((σ m) v)

For a representation of the normal subgroup itself, acting by n and then by m ∈ N is the same as acting by m and then by the conjugate m n m⁻¹: the inner case of TauCeti.Representation.apply_conjNormal_inv.