Module operations on Mᵐᵒᵖ

This file contains definitions that build on top of the group action definitions in GroupTheory.GroupAction.Opposite.

instance MulOpposite.module (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : Module R Mᵐᵒᵖ

MulOpposite.distribMulAction extends to a Module

Equations

• MulOpposite.module R = let src := MulOpposite.distribMulAction M R; Module.mk (_ : ∀ (r₁ r₂ : R) (x : Mᵐᵒᵖ), (r₁ + r₂) • x = r₁ • x + r₂ • x) (_ : ∀ (x : Mᵐᵒᵖ), 0 • x = 0)

def MulOpposite.opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] Mᵐᵒᵖ

The function op is a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulOpposite.coe_opLinearEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(MulOpposite.opLinearEquiv R) = MulOpposite.op

@[simp]

theorem MulOpposite.coe_opLinearEquiv_symm (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = MulOpposite.unop

@[simp]

theorem MulOpposite.coe_opLinearEquiv_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑↑(MulOpposite.opLinearEquiv R) = MulOpposite.op

@[simp]

theorem MulOpposite.coe_opLinearEquiv_symm_toLinearMap (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = MulOpposite.unop

theorem MulOpposite.opLinearEquiv_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : LinearEquiv.toAddEquiv (MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv

@[simp]

theorem MulOpposite.coe_opLinearEquiv_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(MulOpposite.opLinearEquiv R) = MulOpposite.opAddEquiv

theorem MulOpposite.opLinearEquiv_symm_toAddEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : LinearEquiv.toAddEquiv (LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = AddEquiv.symm MulOpposite.opAddEquiv

@[simp]

theorem MulOpposite.coe_opLinearEquiv_symm_addEquiv (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)) = AddEquiv.symm MulOpposite.opAddEquiv