English
There is a G-equivariant isomorphism between leftRegular G ⊗ X and leftRegular G ⊗ trivial G X, given by (g, x) ↦ (g, g^{-1}·x).
Русский
Существует эквивариантное по G-действию изоморфизм между leftRegular G ⊗ X и leftRegular G ⊗ trivial G X, заданный отображением (g, x) ↦ (g, g^{-1}·x).
LaTeX
$$$\bigl(\text{leftRegular } G \otimes X\bigr) \cong \bigl(\text{leftRegular } G \otimes \text{trivial } G X^{V}\bigr),$$$
Lean4
/-- Given `X : Action (Type u) G` for `G` a group, then `G × X` (with `G` acting as left
multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to
`G × X` (with `G` acting as left multiplication on the first factor and trivially on the second).
The isomorphism is given by `(g, x) ↦ (g, g⁻¹ • x)`. -/
@[simps!]
noncomputable def leftRegularTensorIso (X : Action (Type u) G) : leftRegular G ⊗ X ≅ leftRegular G ⊗ trivial G X.V :=
mkIso
(Equiv.toIso
{ toFun g := ⟨g.1, (X.ρ (g.1⁻¹ : G) g.2 : X.V)⟩
invFun g := ⟨g.1, X.ρ g.1 g.2⟩
left_inv _ := Prod.ext rfl <| by simp
right_inv _ := Prod.ext rfl <| by simp }) <|
fun _ => by
ext _
simp only [tensorObj_V, tensor_ρ, types_comp_apply, tensor_apply, ofMulAction_apply]
simp
