Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2020 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser

! This file was ported from Lean 3 source module algebra.module.opposites
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.Equiv
import Mathlib.GroupTheory.GroupAction.Opposite

/-!
# Module operations on `Mᡐᡒᡖ`

This file contains definitions that build on top of the group action definitions in
`GroupRheory.GroupAction.Opposite`.
-/


namespace MulOpposite

universe u v

variable (
R: Type u
R : 
Type u: Type (u+1)
Type u) {
M: Type v
M : 
Type v: Type (v+1)
Type v} [
Semiring: Type ?u.2005 β†’ Type ?u.2005
Semiring 
R: Type u
R] [
AddCommMonoid: Type ?u.5671 β†’ Type ?u.5671
AddCommMonoid 
M: Type v
M] [
Module: (R : Type ?u.13) β†’ (M : Type ?u.12) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.13?u.12)
Module 
R: Type u
R 
M: Type v
M]

/-- `MulOpposite.distribMulAction` extends to a `Module` -/
instance 
module: Module R Mᡐᡒᡖ
module : 
Module: (R : Type ?u.75) β†’ (M : Type ?u.74) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max?u.75?u.74)
Module 
R: Type u
R (
MulOpposite: Type ?u.76 β†’ Type ?u.76
MulOpposite 
M: Type v
M) :=
  { 
MulOpposite.distribMulAction: (Ξ± : Type ?u.116) β†’
  (R : Type ?u.115) β†’
    [inst : Monoid R] β†’ [inst_1 : AddMonoid Ξ±] β†’ [inst_2 : DistribMulAction R Ξ±] β†’ DistribMulAction R αᡐᡒᡖ
MulOpposite.distribMulAction 
M: Type v
M 
R: Type u
R with
    add_smul := fun 
r₁: ?m.1041
r₁ 
rβ‚‚: ?m.1044
rβ‚‚ 
x: ?m.1047
x => 
unop_injective: βˆ€ {Ξ± : Type ?u.1049}, Function.Injective unop
unop_injective <| 
add_smul: βˆ€ {R : Type ?u.1055} {M : Type ?u.1054} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r s : R)
  (x : M), (r + s) β€’ x = r β€’ x + s β€’ x
add_smul 
r₁: ?m.1041
r₁ 
rβ‚‚: ?m.1044
rβ‚‚ (
unop: {Ξ± : Type ?u.1061} β†’ αᡐᡒᡖ β†’ Ξ±
unop 
x: ?m.1047
x)
    zero_smul := fun 
x: ?m.1087
x => 
unop_injective: βˆ€ {Ξ± : Type ?u.1089}, Function.Injective unop
unop_injective <| 
zero_smul: βˆ€ (R : Type ?u.1095) {M : Type ?u.1094} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M), 0 β€’ m = 0
zero_smul 
_: Type ?u.1095
_ (
unop: {Ξ± : Type ?u.1101} β†’ αᡐᡒᡖ β†’ Ξ±
unop 
x: ?m.1087
x) }

/-- The function `op` is a linear equivalence. -/
def 
opLinearEquiv: M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv : 
M: Type v
M ≃ₗ[
R: Type u
R] 
M: Type v
Mᡐᡒᡖ :=
  { 
opAddEquiv: {Ξ± : Type ?u.2206} β†’ [inst : Add Ξ±] β†’ Ξ± ≃+ αᡐᡒᡖ
opAddEquiv with map_smul' := 
MulOpposite.op_smul: βˆ€ {Ξ± : Type ?u.3245} {R : Type ?u.3244} [inst : SMul R Ξ±] (c : R) (a : Ξ±), op (c β€’ a) = c β€’ op a
MulOpposite.op_smul }
#align mul_opposite.op_linear_equiv 
MulOpposite.opLinearEquiv: (R : Type u) β†’ {M : Type v} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
MulOpposite.opLinearEquiv

@[simp]
theorem 
coe_opLinearEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(opLinearEquiv R) = op
coe_opLinearEquiv : (
opLinearEquiv: (R : Type ?u.4262) β†’
  {M : Type ?u.4261} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R : 
M: Type v
M β†’ 
M: Type v
Mᡐᡒᡖ) = 
op: {Ξ± : Type ?u.5569} β†’ Ξ± β†’ αᡐᡒᡖ
op :=
  
rfl: βˆ€ {Ξ± : Sort ?u.5610} {a : Ξ±}, a = a
rfl
#align mul_opposite.coe_op_linear_equiv 
MulOpposite.coe_opLinearEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(opLinearEquiv R) = op
MulOpposite.coe_opLinearEquiv

@[simp]
theorem 
coe_opLinearEquiv_symm: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(LinearEquiv.symm (opLinearEquiv R)) = unop
coe_opLinearEquiv_symm : ((
opLinearEquiv: (R : Type ?u.5706) β†’
  {M : Type ?u.5705} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R).
symm: {R : Type ?u.5771} β†’
  {S : Type ?u.5770} β†’
    {M : Type ?u.5769} β†’
      {Mβ‚‚ : Type ?u.5768} β†’
        [inst : Semiring R] β†’
          [inst_1 : Semiring S] β†’
            [inst_2 : AddCommMonoid M] β†’
              [inst_3 : AddCommMonoid Mβ‚‚] β†’
                {module_M : Module R M} β†’
                  {module_S_Mβ‚‚ : Module S Mβ‚‚} β†’
                    {Οƒ : R β†’+* S} β†’
                      {Οƒ' : S β†’+* R} β†’
                        {re₁ : RingHomInvPair Οƒ Οƒ'} β†’ {reβ‚‚ : RingHomInvPair Οƒ' Οƒ} β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ Mβ‚‚ ≃ₛₗ[Οƒ'] M
symm : 
M: Type v
Mᡐᡒᡖ β†’ 
M: Type v
M) = 
unop: {Ξ± : Type ?u.7179} β†’ αᡐᡒᡖ β†’ Ξ±
unop :=
  
rfl: βˆ€ {Ξ± : Sort ?u.7223} {a : Ξ±}, a = a
rfl
#align mul_opposite.coe_op_linear_equiv_symm 
MulOpposite.coe_opLinearEquiv_symm: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(LinearEquiv.symm (opLinearEquiv R)) = unop
MulOpposite.coe_opLinearEquiv_symm

@[simp]
theorem 
coe_opLinearEquiv_toLinearMap: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑↑(opLinearEquiv R) = op
coe_opLinearEquiv_toLinearMap : ((
opLinearEquiv: (R : Type ?u.7337) β†’
  {M : Type ?u.7336} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R).
toLinearMap: {R : Type ?u.7402} β†’
  {S : Type ?u.7401} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring S] β†’
        {Οƒ : R β†’+* S} β†’
          {Οƒ' : S β†’+* R} β†’
            [inst_2 : RingHomInvPair Οƒ Οƒ'] β†’
              [inst_3 : RingHomInvPair Οƒ' Οƒ] β†’
                {M : Type ?u.7400} β†’
                  {Mβ‚‚ : Type ?u.7399} β†’
                    [inst_4 : AddCommMonoid M] β†’
                      [inst_5 : AddCommMonoid Mβ‚‚] β†’
                        [inst_6 : Module R M] β†’ [inst_7 : Module S Mβ‚‚] β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ M β†’β‚›β‚—[Οƒ] Mβ‚‚
toLinearMap : 
M: Type v
M β†’ 
M: Type v
Mᡐᡒᡖ) = 
op: {Ξ± : Type ?u.7914} β†’ Ξ± β†’ αᡐᡒᡖ
op :=
  
rfl: βˆ€ {Ξ± : Sort ?u.7955} {a : Ξ±}, a = a
rfl
#align mul_opposite.coe_op_linear_equiv_to_linear_map 
MulOpposite.coe_opLinearEquiv_toLinearMap: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑↑(opLinearEquiv R) = op
MulOpposite.coe_opLinearEquiv_toLinearMap

@[simp]
theorem 
coe_opLinearEquiv_symm_toLinearMap: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑↑(LinearEquiv.symm (opLinearEquiv R)) = unop
coe_opLinearEquiv_symm_toLinearMap :
    ((
opLinearEquiv: (R : Type ?u.8048) β†’
  {M : Type ?u.8047} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R).
symm: {R : Type ?u.8113} β†’
  {S : Type ?u.8112} β†’
    {M : Type ?u.8111} β†’
      {Mβ‚‚ : Type ?u.8110} β†’
        [inst : Semiring R] β†’
          [inst_1 : Semiring S] β†’
            [inst_2 : AddCommMonoid M] β†’
              [inst_3 : AddCommMonoid Mβ‚‚] β†’
                {module_M : Module R M} β†’
                  {module_S_Mβ‚‚ : Module S Mβ‚‚} β†’
                    {Οƒ : R β†’+* S} β†’
                      {Οƒ' : S β†’+* R} β†’
                        {re₁ : RingHomInvPair Οƒ Οƒ'} β†’ {reβ‚‚ : RingHomInvPair Οƒ' Οƒ} β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ Mβ‚‚ ≃ₛₗ[Οƒ'] M
symm.
toLinearMap: {R : Type ?u.8229} β†’
  {S : Type ?u.8228} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring S] β†’
        {Οƒ : R β†’+* S} β†’
          {Οƒ' : S β†’+* R} β†’
            [inst_2 : RingHomInvPair Οƒ Οƒ'] β†’
              [inst_3 : RingHomInvPair Οƒ' Οƒ] β†’
                {M : Type ?u.8227} β†’
                  {Mβ‚‚ : Type ?u.8226} β†’
                    [inst_4 : AddCommMonoid M] β†’
                      [inst_5 : AddCommMonoid Mβ‚‚] β†’
                        [inst_6 : Module R M] β†’ [inst_7 : Module S Mβ‚‚] β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ M β†’β‚›β‚—[Οƒ] Mβ‚‚
toLinearMap : 
M: Type v
Mᡐᡒᡖ β†’ 
M: Type v
M) = 
unop: {Ξ± : Type ?u.8731} β†’ αᡐᡒᡖ β†’ Ξ±
unop :=
  
rfl: βˆ€ {Ξ± : Sort ?u.8775} {a : Ξ±}, a = a
rfl
#align mul_opposite.coe_op_linear_equiv_symm_to_linear_map 
MulOpposite.coe_opLinearEquiv_symm_toLinearMap: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑↑(LinearEquiv.symm (opLinearEquiv R)) = unop
MulOpposite.coe_opLinearEquiv_symm_toLinearMap

-- Porting note: LHS simplifies; added new simp lemma below @[simp]
theorem 
opLinearEquiv_toAddEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearEquiv.toAddEquiv (opLinearEquiv R) = opAddEquiv
opLinearEquiv_toAddEquiv : (
opLinearEquiv: (R : Type ?u.9049) β†’
  {M : Type ?u.9048} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R : 
M: Type v
M ≃ₗ[
R: Type u
R] 
M: Type v
Mᡐᡒᡖ).
toAddEquiv: {R : Type ?u.9125} β†’
  {S : Type ?u.9124} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring S] β†’
        {Οƒ : R β†’+* S} β†’
          {Οƒ' : S β†’+* R} β†’
            [inst_2 : RingHomInvPair Οƒ Οƒ'] β†’
              [inst_3 : RingHomInvPair Οƒ' Οƒ] β†’
                {M : Type ?u.9123} β†’
                  {Mβ‚‚ : Type ?u.9122} β†’
                    [inst_4 : AddCommMonoid M] β†’
                      [inst_5 : AddCommMonoid Mβ‚‚] β†’
                        [inst_6 : Module R M] β†’ [inst_7 : Module S Mβ‚‚] β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ M ≃+ Mβ‚‚
toAddEquiv = 
opAddEquiv: {Ξ± : Type ?u.9155} β†’ [inst : Add Ξ±] β†’ Ξ± ≃+ αᡐᡒᡖ
opAddEquiv :=
  
rfl: βˆ€ {Ξ± : Sort ?u.9711} {a : Ξ±}, a = a
rfl
#align mul_opposite.op_linear_equiv_to_add_equiv 
MulOpposite.opLinearEquiv_toAddEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearEquiv.toAddEquiv (opLinearEquiv R) = opAddEquiv
MulOpposite.opLinearEquiv_toAddEquiv

@[simp]
theorem 
coe_opLinearEquiv_addEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(opLinearEquiv R) = opAddEquiv
coe_opLinearEquiv_addEquiv : ((
opLinearEquiv: (R : Type ?u.10763) β†’
  {M : Type ?u.10762} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R : 
M: Type v
M ≃ₗ[
R: Type u
R] 
M: Type v
Mᡐᡒᡖ) : 
M: Type v
M ≃+ 
M: Type v
Mᡐᡒᡖ) = 
opAddEquiv: {Ξ± : Type ?u.11064} β†’ [inst : Add Ξ±] β†’ Ξ± ≃+ αᡐᡒᡖ
opAddEquiv :=
  
rfl: βˆ€ {Ξ± : Sort ?u.11156} {a : Ξ±}, a = a
rfl

-- Porting note: LHS simplifies; added new simp lemma below @[simp]
theorem 
opLinearEquiv_symm_toAddEquiv: LinearEquiv.toAddEquiv (LinearEquiv.symm (opLinearEquiv R)) = AddEquiv.symm opAddEquiv
opLinearEquiv_symm_toAddEquiv :
    (
opLinearEquiv: (R : Type ?u.11433) β†’
  {M : Type ?u.11432} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R : 
M: Type v
M ≃ₗ[
R: Type u
R] 
M: Type v
Mᡐᡒᡖ).
symm: {R : Type ?u.11509} β†’
  {S : Type ?u.11508} β†’
    {M : Type ?u.11507} β†’
      {Mβ‚‚ : Type ?u.11506} β†’
        [inst : Semiring R] β†’
          [inst_1 : Semiring S] β†’
            [inst_2 : AddCommMonoid M] β†’
              [inst_3 : AddCommMonoid Mβ‚‚] β†’
                {module_M : Module R M} β†’
                  {module_S_Mβ‚‚ : Module S Mβ‚‚} β†’
                    {Οƒ : R β†’+* S} β†’
                      {Οƒ' : S β†’+* R} β†’
                        {re₁ : RingHomInvPair Οƒ Οƒ'} β†’ {reβ‚‚ : RingHomInvPair Οƒ' Οƒ} β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ Mβ‚‚ ≃ₛₗ[Οƒ'] M
symm.
toAddEquiv: {R : Type ?u.11527} β†’
  {S : Type ?u.11526} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring S] β†’
        {Οƒ : R β†’+* S} β†’
          {Οƒ' : S β†’+* R} β†’
            [inst_2 : RingHomInvPair Οƒ Οƒ'] β†’
              [inst_3 : RingHomInvPair Οƒ' Οƒ] β†’
                {M : Type ?u.11525} β†’
                  {Mβ‚‚ : Type ?u.11524} β†’
                    [inst_4 : AddCommMonoid M] β†’
                      [inst_5 : AddCommMonoid Mβ‚‚] β†’
                        [inst_6 : Module R M] β†’ [inst_7 : Module S Mβ‚‚] β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ M ≃+ Mβ‚‚
toAddEquiv = 
opAddEquiv: {Ξ± : Type ?u.11557} β†’ [inst : Add Ξ±] β†’ Ξ± ≃+ αᡐᡒᡖ
opAddEquiv.
symm: {M : Type ?u.11588} β†’ {N : Type ?u.11587} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ M ≃+ N β†’ N ≃+ M
symm :=
  
rfl: βˆ€ {Ξ± : Sort ?u.12603} {a : Ξ±}, a = a
rfl
#align mul_opposite.op_linear_equiv_symm_to_add_equiv 
MulOpposite.opLinearEquiv_symm_toAddEquiv: βˆ€ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearEquiv.toAddEquiv (LinearEquiv.symm (opLinearEquiv R)) = AddEquiv.symm opAddEquiv
MulOpposite.opLinearEquiv_symm_toAddEquiv

@[simp]
theorem 
coe_opLinearEquiv_symm_addEquiv: ↑(LinearEquiv.symm (opLinearEquiv R)) = AddEquiv.symm opAddEquiv
coe_opLinearEquiv_symm_addEquiv :
    ((
opLinearEquiv: (R : Type ?u.13655) β†’
  {M : Type ?u.13654} β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst_2 : Module R M] β†’ M ≃ₗ[R] Mᡐᡒᡖ
opLinearEquiv 
R: Type u
R : 
M: Type v
M ≃ₗ[
R: Type u
R] 
M: Type v
Mᡐᡒᡖ).
symm: {R : Type ?u.13731} β†’
  {S : Type ?u.13730} β†’
    {M : Type ?u.13729} β†’
      {Mβ‚‚ : Type ?u.13728} β†’
        [inst : Semiring R] β†’
          [inst_1 : Semiring S] β†’
            [inst_2 : AddCommMonoid M] β†’
              [inst_3 : AddCommMonoid Mβ‚‚] β†’
                {module_M : Module R M} β†’
                  {module_S_Mβ‚‚ : Module S Mβ‚‚} β†’
                    {Οƒ : R β†’+* S} β†’
                      {Οƒ' : S β†’+* R} β†’
                        {re₁ : RingHomInvPair Οƒ Οƒ'} β†’ {reβ‚‚ : RingHomInvPair Οƒ' Οƒ} β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ Mβ‚‚ ≃ₛₗ[Οƒ'] M
symm : 
M: Type v
Mᡐᡒᡖ ≃+ 
M: Type v
M) = 
opAddEquiv: {Ξ± : Type ?u.13989} β†’ [inst : Add Ξ±] β†’ Ξ± ≃+ αᡐᡒᡖ
opAddEquiv.
symm: {M : Type ?u.14020} β†’ {N : Type ?u.14019} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ M ≃+ N β†’ N ≃+ M
symm :=
  
rfl: βˆ€ {Ξ± : Sort ?u.14217} {a : Ξ±}, a = a
rfl

end MulOpposite