def LinearMap.op {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) : Mᵐᵒᵖ →ₛₗ[σ] M₂ᵐᵒᵖ

Equations

• f.op = { toFun := fun (x : Mᵐᵒᵖ) => MulOpposite.op (f (MulOpposite.unop x)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.op_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) (x : Mᵐᵒᵖ) : f.op x = MulOpposite.op (f (MulOpposite.unop x))

def LinearMap.unop {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : Mᵐᵒᵖ →ₛₗ[σ] M₂ᵐᵒᵖ) : M →ₛₗ[σ] M₂

Equations

• f.unop = { toFun := fun (x : M) => MulOpposite.unop (f (MulOpposite.op x)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.unop_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : Mᵐᵒᵖ →ₛₗ[σ] M₂ᵐᵒᵖ) (x : M) : f.unop x = MulOpposite.unop (f (MulOpposite.op x))

@[simp]

theorem LinearMap.unop_op {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : Mᵐᵒᵖ →ₛₗ[σ] M₂ᵐᵒᵖ) : f.unop.op = f

@[simp]

theorem LinearMap.op_unop {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) : f.op.unop = f

@[simp]

theorem AlgEquiv.op_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : (AlgEquiv.op f).toLinearMap = f.toLinearMap.op