Equivariant equivalences of additive groups

This file records elementary facts about additive equivalences that intertwine group actions.

Main results

• AddEquiv.symm_map_smul_of_map_smul: the inverse of an equivariant additive equivalence is equivariant.
• AddEquiv.symm_map_smul_of_map_mulEquiv_smul: the same along a change of the acting group by a multiplicative equivalence.
• AddEquiv.ofBijective_smul: the additive equivalence of a bijective equivariant homomorphism is equivariant, and AddEquiv.ofBijective_toDistribMulActionHom identifies the equivariant homomorphism it carries with the original one.

theorem AddEquiv.symm_map_smul_of_map_smul {G : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] [SMul G M] [SMul G N] (e : M ≃+ N) (hequiv : ∀ (g : G) (m : M), e (g • m) = g • e m) (g : G) (n : N) : e.symm (g • n) = g • e.symm n

The inverse of an equivariant additive equivalence is equivariant.

theorem AddEquiv.symm_map_smul_of_map_mulEquiv_smul {G : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [Mul G] [Mul H] [Add M] [Add N] [SMul G M] [SMul H N] (e : M ≃+ N) (φ : H ≃* G) (hequiv : ∀ (h : H) (m : M), e (φ h • m) = h • e m) (g : G) (n : N) : e.symm (φ.symm g • n) = g • e.symm n

The inverse of an additive equivalence compatible with a change of the acting group is compatible with the inverse change: if e (φ h • m) = h • e m for a multiplicative equivalence φ : H ≃* G, then e.symm (φ.symm g • n) = g • e.symm n.

theorem AddEquiv.ofBijective_smul {G : Type u_1} {M : Type u_2} {N : Type u_3} [Monoid G] [AddMonoid M] [AddMonoid N] [DistribMulAction G M] [DistribMulAction G N] {f : M →+[G] N} (hf : Function.Bijective ⇑f) (g : G) (m : M) : (ofBijective (↑f) hf) (g • m) = g • (ofBijective (↑f) hf) m

The additive equivalence of a bijective equivariant homomorphism is equivariant. The statement is spelled on the equivalence so that it can be fed to constructions that take an equivariant additive equivalence.

theorem AddEquiv.ofBijective_toDistribMulActionHom {G : Type u_1} {M : Type u_2} {N : Type u_3} [Monoid G] [AddMonoid M] [AddMonoid N] [DistribMulAction G M] [DistribMulAction G N] {f : M →+[G] N} (hf : Function.Bijective ⇑f) : (let __src := (ofBijective (↑f) hf).toAddMonoidHom; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) = f

The equivariant homomorphism carried by the additive equivalence of a bijective equivariant homomorphism is that homomorphism.