English
Alternate formulation of the inverse isomorphism action on a basis element.
Русский
Альтернативная формулировка действия обратного изоморфизма на базисный элемент.
LaTeX
$$MonoidAlgebra.opRingEquiv_symm_single (r : k^{op}) (x : G^{op}) : \\mathrm{opRingEquiv}.symm (single x r) = op (single x.unop r.unop)$$
Lean4
/-- The opposite of an `R[I]` is ring equivalent to
the `AddMonoidAlgebra Rᵐᵒᵖ I` over the opposite ring, taking elements to their opposite. -/
@[simps! +simpRhs apply symm_apply]
protected noncomputable def opRingEquiv [AddCommMagma G] : k[G]ᵐᵒᵖ ≃+* kᵐᵒᵖ[G] :=
{ opAddEquiv.symm.trans (mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)) with
map_mul' :=
by
let f : k[G]ᵐᵒᵖ ≃+ kᵐᵒᵖ[G] := opAddEquiv.symm.trans (mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ))
change ∀ (x y : k[G]ᵐᵒᵖ), f (x * y) = f x * f y
rw [← AddEquiv.coe_toAddMonoidHom, AddMonoidHom.map_mul_iff]
ext i₁ r₁ i₂ r₂ : 6
dsimp only [f, AddMonoidHom.compr₂_apply, AddMonoidHom.compl₂_apply, AddMonoidHom.comp_apply,
AddMonoidHom.coe_coe, AddEquiv.toAddMonoidHom_eq_coe, AddEquiv.coe_addMonoidHom_trans, singleAddHom_apply,
opAddEquiv_apply, opAddEquiv_symm_apply, AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft, unop_mul, unop_op]
-- Defeq abuse. Probably `k[G]` vs `G →₀ k`.
erw [mapRange.addEquiv_apply, mapRange.addEquiv_apply, mapRange.addEquiv_apply]
rw [single_mul_single, mapRange_single, mapRange_single, mapRange_single, single_mul_single]
simp only [opAddEquiv_apply, op_mul, add_comm] }
-- Not `@[simp]` because the LHS simplifies further.
-- TODO: the LHS simplifies to `Finsupp.single`, which implies there's some defeq abuse going on.
