Mathlib.Algebra.Module.Equiv.Opposite

LinearMap.ext_ring_op theorem

{σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M} (h : f (1 : R) = g (1 : R)) : f = g

Full source

@[ext high]
theorem LinearMap.ext_ring_op
    {σ : RᵐᵒᵖRᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M} (h : f (1 : R) = g (1 : R)) :
    f = g :=
  ext fun x ↦ by
    rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

Equality of linear maps determined by their value at 1

Informal description

Let $R$ and $S$ be semirings, and let $\sigma: R^\text{op} \to S$ be a ring homomorphism from the multiplicative opposite of $R$ to $S$. For any two $\sigma$-linear maps $f, g: R \to M$ (where $M$ is an $S$-module), if $f(1) = g(1)$, then $f = g$.

MulOpposite.opLinearEquiv definition

: M ≃ₗ[R] Mᵐᵒᵖ

Full source

/-- The function `op` is a linear equivalence. -/
def opLinearEquiv : M ≃ₗ[R] Mᵐᵒᵖ :=
  { opAddEquiv with map_smul' := MulOpposite.op_smul }

Linear equivalence between a module and its multiplicative opposite

Informal description

The function $\text{op} : M \to M^\text{op}$ is a linear equivalence between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$. Here, $M^\text{op}$ is equipped with the module structure where scalar multiplication is defined by $r \cdot \text{op}(m) = \text{op}(r \cdot m)$ for all $r \in R$ and $m \in M$.

MulOpposite.coe_opLinearEquiv theorem

: (opLinearEquiv R : M → Mᵐᵒᵖ) = op

Full source

@[simp]
theorem coe_opLinearEquiv : (opLinearEquiv R : M → Mᵐᵒᵖ) = op :=
  rfl

Underlying Function of Linear Equivalence to Multiplicative Opposite is Canonical Embedding

Informal description

The underlying function of the linear equivalence $\text{opLinearEquiv}_R$ from a module $M$ to its multiplicative opposite $M^\text{op}$ is equal to the canonical embedding $\text{op} : M \to M^\text{op}$.

MulOpposite.coe_opLinearEquiv_symm theorem

: ((opLinearEquiv R).symm : Mᵐᵒᵖ → M) = unop

Full source

@[simp]
theorem coe_opLinearEquiv_symm : ((opLinearEquiv R).symm : Mᵐᵒᵖ → M) = unop :=
  rfl

Inverse of Module-Opposite Linear Equivalence is Canonical Projection

Informal description

The inverse of the linear equivalence $\text{opLinearEquiv}_R : M \simeq M^\text{op}$ between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$ is equal to the canonical projection $\text{unop} : M^\text{op} \to M$.

MulOpposite.coe_opLinearEquiv_toLinearMap theorem

: ((opLinearEquiv R).toLinearMap : M → Mᵐᵒᵖ) = op

Full source

@[simp]
theorem coe_opLinearEquiv_toLinearMap : ((opLinearEquiv R).toLinearMap : M → Mᵐᵒᵖ) = op :=
  rfl

Linear map of the module-multiplicative opposite equivalence is the canonical embedding

Informal description

The underlying linear map of the linear equivalence $\text{opLinearEquiv}_R : M \to M^\text{op}$ is equal to the canonical embedding $\text{op} : M \to M^\text{op}$.

MulOpposite.coe_opLinearEquiv_symm_toLinearMap theorem

: ((opLinearEquiv R).symm.toLinearMap : Mᵐᵒᵖ → M) = unop

Full source

@[simp]
theorem coe_opLinearEquiv_symm_toLinearMap :
    ((opLinearEquiv R).symm.toLinearMap : Mᵐᵒᵖ → M) = unop :=
  rfl

Inverse of Linear Equivalence to Opposite Module as Canonical Projection

Informal description

The linear map associated with the inverse of the linear equivalence $\text{opLinearEquiv}_R : M \simeq_{R} M^\text{op}$ is equal to the canonical projection $\text{unop} : M^\text{op} \to M$.

MulOpposite.opLinearEquiv_toAddEquiv theorem

: (opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).toAddEquiv = opAddEquiv

Full source

theorem opLinearEquiv_toAddEquiv : (opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).toAddEquiv = opAddEquiv :=
  rfl

Additive Equivalence Component of $\text{opLinearEquiv}_R$ Equals $\text{opAddEquiv}$

Informal description

The additive equivalence component of the linear equivalence $\text{opLinearEquiv}_R : M \simeq_{R} M^\text{op}$ between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$ is equal to the additive equivalence $\text{opAddEquiv} : M \simeq_{+} M^\text{op}$.

MulOpposite.coe_opLinearEquiv_addEquiv theorem

: ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ) : M ≃+ Mᵐᵒᵖ) = opAddEquiv

Full source

@[simp]
theorem coe_opLinearEquiv_addEquiv : ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ) : M ≃+ Mᵐᵒᵖ) = opAddEquiv :=
  rfl

Additive Equivalence Underlying the Linear Equivalence Between a Module and Its Opposite

Informal description

The underlying additive equivalence of the linear equivalence $\text{opLinearEquiv}_R : M \simeq_{R} M^\text{op}$ between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$ is equal to the additive equivalence $\text{opAddEquiv} : M \simeq^+ M^\text{op}$.

MulOpposite.opLinearEquiv_symm_toAddEquiv theorem

: (opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm.toAddEquiv = opAddEquiv.symm

Full source

theorem opLinearEquiv_symm_toAddEquiv :
    (opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm.toAddEquiv = opAddEquiv.symm :=
  rfl

Additive Equivalence Component of Inverse Linear Equivalence Between Module and Its Opposite

Informal description

The additive equivalence component of the inverse of the linear equivalence $\text{opLinearEquiv}_R : M \simeq_{R} M^\text{op}$ between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$ is equal to the inverse of the additive equivalence $\text{opAddEquiv} : M \simeq_{+} M^\text{op}$.

MulOpposite.coe_opLinearEquiv_symm_addEquiv theorem

: ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm : Mᵐᵒᵖ ≃+ M) = opAddEquiv.symm

Full source

@[simp]
theorem coe_opLinearEquiv_symm_addEquiv :
    ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ).symm : MᵐᵒᵖMᵐᵒᵖ ≃+ M) = opAddEquiv.symm :=
  rfl

Additive Equivalence of Inverse Linear Equivalence Between Module and Its Opposite

Informal description

The underlying additive equivalence of the inverse of the linear equivalence $\text{opLinearEquiv}_R : M \simeq_{R} M^\text{op}$ between a module $M$ over a semiring $R$ and its multiplicative opposite $M^\text{op}$ is equal to the inverse of the additive equivalence $\text{opAddEquiv} : M \simeq^+ M^\text{op}$.