mathlib documentation

algebra.module.opposites

Module operations on `Mᵒᵖ` #

This file contains definitions that could not be placed into algebra.opposites due to import cycles.

@[instance]

def opposite.module (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

module R Mᵒᵖ

opposite.distrib_mul_action extends to a module

Equations

opposite.module R = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (opposite.distrib_mul_action M R), smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

def opposite.op_linear_equiv (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

M ≃ₗ[R] Mᵒᵖ

The function op is a linear equivalence.

Equations

opposite.op_linear_equiv R = {to_fun := opposite.op_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := opposite.op_add_equiv.inv_fun, left_inv := _, right_inv := _}

@[simp]

theorem opposite.coe_op_linear_equiv (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

⇑(opposite.op_linear_equiv R) = opposite.op

@[simp]

theorem opposite.coe_op_linear_equiv_symm (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

⇑((opposite.op_linear_equiv R).symm) = opposite.unop

@[simp]

theorem opposite.coe_op_linear_equiv_to_linear_map (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

⇑((opposite.op_linear_equiv R).to_linear_map) = opposite.op

@[simp]

theorem opposite.coe_op_linear_equiv_symm_to_linear_map (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

⇑((opposite.op_linear_equiv R).symm.to_linear_map) = opposite.unop

@[simp]

theorem opposite.op_linear_equiv_to_add_equiv (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

(opposite.op_linear_equiv R).to_add_equiv = opposite.op_add_equiv

@[simp]

theorem opposite.op_linear_equiv_symm_to_add_equiv (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

(opposite.op_linear_equiv R).symm.to_add_equiv = opposite.op_add_equiv.symm