Theorems · Definition · group theory
Rep.applyAsHom
{k : Type u} → [inst : Semiring k] → {G : Type v} → [inst_1 : CommMonoid G] → (A : Rep.{u_1, u, v} k G) → G → (A ⟶ A)Given a representation A of a commutative monoid G, the map ρ_A(g) is a representation
morphism A ⟶ A for any g : G.
- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement · cited by 32,603
- Semiringstatement and proof · cited by 13,802
- CommMonoidstatement and proof · cited by 2,264
- Repstatement and proof · cited by 843
- Rep.ρproof · cited by 356
- Rep.ofHomproof · cited by 45
Cited by26
Results whose statement or proof uses this declaration.
- Rep.FiniteCyclicGroup.normHomCompSubproof · cited by 4
- Rep.FiniteCyclicGroup.subCompNormHomproof · cited by 4
- Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombinationstatement and proof · cited by 2
- Rep.applyAsHom_commstatement · cited by 2
- Rep.FiniteCyclicGroup.groupCohomologyπEvenstatement · cited by 2
- Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iffstatement and proof · cited by 2
- Rep.FiniteCyclicGroup.groupHomologyπOddstatement · cited by 2
- Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_normstatement · cited by 1
- Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_substatement and proof · cited by 1
- Rep.applyAsHom_applystatement · cited by 1
- Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iffstatement and proof · cited by 1
- Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iffstatement and proof · cited by 1