conj_ρ — Mathlib

English

For any isomorphism of actions f: M ≅ N, the action maps ρ_g are conjugate via the forgetful functor.

Русский

Для изоморфизма действий f: M ≅ N отображения действия ρ_g сопряжены через забывающий функтор.

LaTeX

$$theorem conj_ρ {M,N} (f : M ≅ N) (g : G) : N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)$$

Lean4

theorem conj_ρ {M N : Action V G} (f : M ≅ N) (g : G) : N.ρ g = ((forget V G).mapIso f).conj (M.ρ g) := by
  rw [Iso.conj_apply, Iso.eq_inv_comp]; simp [f.hom.comm]

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