coe_linearization_obj_ρ — Mathlib

English

For any g ∈ G, the coefficient extraction functor applied to the ρ-action on X yields the same as mapping the coefficient via X.ρ g; i.e., DFunLike.coe ρ(g) = A.ρ(f g) on coefficients.

Русский

Для любого g ∈ G коэффициентное отображение сочетается с действием ρ: коэффициент в линейлизации соответствует коэффициенту после применения X.ρ g.

LaTeX

$$$\mathrm{DFunLike}.\mathrm{coe}\ (\rho(g)) = A.\rho(f g)$$$

Lean4

@[simp]
theorem coe_linearization_obj_ρ (X : Action (Type u) G) (g : G) :
    @DFunLike.coe (no_index G →* ((X.V →₀ k) →ₗ[k] (X.V →₀ k))) _ (fun _ => (X.V →₀ k) →ₗ[k] (X.V →₀ k)) _
        ((linearization k G).obj X).ρ g =
      Finsupp.lmapDomain k k (X.ρ g) :=
  rfl

Похожие утверждения