Theorems · Theorem · group theory

Rep.invariantsAdjunction_homEquiv_apply_hom

∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] {X : ModuleCat k} {Y : Rep.{u_1, u, v} k G}
  (f : (Rep.trivialFunctor k G).obj X ⟶ Y),
  ModuleCat.Hom.hom (((Rep.invariantsAdjunction k G).homEquiv X Y) f) =
    LinearMap.codRestrict Y.ρ.invariants (Rep.Hom.hom f).toLinearMap ⋯

Defined in

Mathlib.RepresentationTheory.Invariants

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroup