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.mul_zero_class.to_opposite_smul_with_zero (R : Type u) [mul_zero_class R] :

smul_with_zero Rᵒᵖ R

Like mul_zero_class.to_smul_with_zero, but multiplies on the right.

Equations

opposite.mul_zero_class.to_opposite_smul_with_zero R = {to_has_scalar := {smul := λ (c : Rᵒᵖ) (x : R), x * opposite.unop c}, smul_zero := _, zero_smul := _}

@[instance]

def opposite.monoid_with_zero.to_opposite_mul_action_with_zero (R : Type u) [monoid_with_zero R] :

mul_action_with_zero Rᵒᵖ R

Like monoid_with_zero.to_mul_action_with_zero, but multiplies on the right.

Equations

opposite.monoid_with_zero.to_opposite_mul_action_with_zero R = {to_mul_action := {to_has_scalar := smul_with_zero.to_has_scalar (opposite.mul_zero_class.to_opposite_smul_with_zero R), one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

@[instance]

def opposite.semiring.to_opposite_module (R : Type u) [semiring R] :

module Rᵒᵖ R

Like semiring.to_module, but multiplies on the right.

Equations

opposite.semiring.to_opposite_module R = {to_distrib_mul_action := {to_mul_action := opposite.monoid.to_opposite_mul_action R (monoid_with_zero.to_monoid R), smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

@[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