Unopposing a commutative group

Mathlib's MulOpposite.opMulEquiv identifies a commutative monoid with its opposite when the commutativity is available as a CommMonoid instance. This file provides the explicit-hypothesis variant: for a monoid whose multiplication commutes, as a hypothesis rather than an instance, the unopposite map is a monoid isomorphism. This is what makes the opposite disappear in comparisons such as TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv, where the deck group is commutative by a proof, not by an instance.

def TauCeti.MulOpposite.unopMulEquivOfComm {G : Type u_1} [Monoid G] (hcomm : ∀ (a b : G), a * b = b * a) : Gᵐᵒᵖ ≃* G

The unopposite map on a monoid whose multiplication commutes is a monoid isomorphism. This is the explicit-hypothesis variant of MulOpposite.opMulEquiv.symm, for monoids whose commutativity is a hypothesis rather than a CommMonoid instance.

Equations

• TauCeti.MulOpposite.unopMulEquivOfComm hcomm = { toEquiv := MulOpposite.opEquiv.symm, map_mul' := ⋯ }

@[simp]

theorem TauCeti.MulOpposite.unopMulEquivOfComm_apply {G : Type u_1} [Monoid G] (hcomm : ∀ (a b : G), a * b = b * a) (d : Gᵐᵒᵖ) : (unopMulEquivOfComm hcomm) d = MulOpposite.unop d

@[simp]

theorem TauCeti.MulOpposite.unopMulEquivOfComm_symm_apply {G : Type u_1} [Monoid G] (hcomm : ∀ (a b : G), a * b = b * a) (a : G) : (unopMulEquivOfComm hcomm).symm a = MulOpposite.op a