Mathlib.Algebra.Module.Equiv.Defs

LinearEquiv structure

{R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
  {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*)
  [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap σ M M₂, M ≃+ M₂

Full source

/-- A linear equivalence is an invertible linear map. -/
structure LinearEquiv {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
  {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*)
  [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap σ M M₂, M ≃+ M₂

Linear Equivalence (Semilinear Isomorphism)

Informal description

A linear equivalence is an invertible linear map between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$. It consists of a semilinear map that preserves the module structure up to the action of $\sigma$, along with an additive equivalence between $M$ and $M_2$. More precisely, given: - Semirings $R$ and $S$, - A ring homomorphism $\sigma: R \to S$ and its inverse pair $\sigma': S \to R$ satisfying certain compatibility conditions, - Additive commutative monoids $M$ and $M_2$ equipped with module structures over $R$ and $S$ respectively, a linear equivalence $e: M \simeq_{\sigma} M_2$ is an invertible map satisfying $e (r \cdot x) = \sigma(r) \cdot e(x)$ for all $r \in R$ and $x \in M$.

term_≃ₛₗ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M ≃ₛₗ[σ] M₂` denotes the type of linear equivalences between `M` and `M₂` over a
ring homomorphism `σ`. -/
notation:50 M " ≃ₛₗ[" σ "] " M₂ => LinearEquiv σ M M₂

Semilinear equivalence notation

Informal description

The notation $ M \simeq_{\sigma} M_2 $ denotes the type of semilinear equivalences between modules $ M $ and $ M_2 $ over a ring homomorphism $ \sigma $. A semilinear equivalence is an invertible semilinear map that preserves the module structure up to the action of $ \sigma $.

term_≃ₗ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M ≃ₗ[R] M₂` denotes the type of linear equivalences between `M` and `M₂` over
a plain linear map `M →ₗ M₂`. -/
notation:50 M " ≃ₗ[" R "] " M₂ => LinearEquiv (RingHom.id R) M M₂

Linear equivalence over a ring

Informal description

The notation $ M \simeq_{R} M_2 $ denotes the type of linear equivalences between $ M $ and $ M_2 $ over the ring $ R $, which are invertible linear maps $ M \to M_2 $.

SemilinearEquivClass structure

(F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
  (σ : outParam <| R →+* S) {σ' : outParam <| S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
  (M M₂ : outParam Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
  [EquivLike F M M₂] : Prop
  extends AddEquivClass F M M₂

Full source

/-- `SemilinearEquivClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear equivs
`M → M₂`.

See also `LinearEquivClass F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. -/
class SemilinearEquivClass (F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
  (σ : outParam <| R →+* S) {σ' : outParam <| S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
  (M M₂ : outParam Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
  [EquivLike F M M₂] : Prop
  extends AddEquivClass F M M₂ where
  /-- Applying a semilinear equivalence `f` over `σ` to `r • x` equals `σ r • f x`. -/
  map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x

Class of Semilinear Equivalences

Informal description

The class `SemilinearEquivClass F σ M M₂` asserts that `F` is a type of bundled `σ`-semilinear equivalences between modules `M` and `M₂`, where `σ` is a ring homomorphism from `R` to `S`. A map `f : M → M₂` in this class satisfies the following properties: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Semilinearity: $f(c \bullet x) = (\sigma c) \bullet f(x)$ for all $c \in R$ and $x \in M$ 3. Bijectivity: `f` is a bijection between `M` and `M₂` Here, `M` is an `R`-module, `M₂` is an `S`-module, and the ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` satisfy the inverse pair conditions `σ ∘ σ' = id` and `σ' ∘ σ = id`.

LinearEquivClass abbrev

 (F : Type*) (R M M₂ : outParam Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
  [EquivLike F M M₂]

Full source

/-- `LinearEquivClass F R M M₂` asserts `F` is a type of bundled `R`-linear equivs `M → M₂`.
This is an abbreviation for `SemilinearEquivClass F (RingHom.id R) M M₂`.
-/
abbrev LinearEquivClass (F : Type*) (R M M₂ : outParam Type*) [Semiring R] [AddCommMonoid M]
    [AddCommMonoid M₂] [Module R M] [Module R M₂] [EquivLike F M M₂] :=
  SemilinearEquivClass F (RingHom.id R) M M₂

Class of $R$-Linear Equivalences Between Modules

Informal description

The class `LinearEquivClass F R M M₂` asserts that `F` is a type of bundled $R$-linear equivalences between $R$-modules `M` and `M₂`. A map $f \in F$ satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Linearity: $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in M$ 3. Bijectivity: $f$ is a bijection between $M$ and $M₂$ Here, $M$ and $M₂$ are $R$-modules, and $R$ is a semiring.

SemilinearEquivClass.instSemilinearMapClass instance

 [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [s : SemilinearEquivClass F σ M M₂] :
  SemilinearMapClass F σ M M₂

Full source

instance (priority := 100) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
  [EquivLike F M M₂] [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂ :=
  { s with }

Semilinear Equivalences as Semilinear Maps

Informal description

For any type `F` that is a `SemilinearEquivClass` with ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` forming inverse pairs, and modules `M` over `R` and `M₂` over `S`, there exists a corresponding `SemilinearMapClass` instance for `F`. This means that any `σ`-semilinear equivalence between `M` and `M₂` can be treated as a `σ`-semilinear map, preserving the additive and scalar multiplication structures with respect to the ring homomorphism `σ`.

SemilinearEquivClass.semilinearEquiv definition

 [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] (f : F) : M ≃ₛₗ[σ] M₂

Full source

/-- Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence. -/
@[coe]
def semilinearEquiv [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] (f : F) : M ≃ₛₗ[σ] M₂ :=
  { (f : M ≃+ M₂), (f : M →ₛₗ[σ] M₂) with }

Semilinear equivalence realization from class element

Informal description

Given a type `F` that is a `SemilinearEquivClass` with ring homomorphisms $\sigma: R \to S$ and $\sigma': S \to R$ forming inverse pairs, and modules $M$ over $R$ and $M_2$ over $S$, any element $f \in F$ can be reinterpreted as a semilinear equivalence $M \simeq_{\sigma} M_2$. This equivalence consists of: 1. An additive equivalence $f: M \simeq^+ M_2$ between the additive groups of $M$ and $M_2$ 2. A semilinear map $f: M \to_{\sigma} M_2$ that satisfies $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all $r \in R$ and $x \in M$

SemilinearEquivClass.instCoeToSemilinearEquiv instance

 [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] :
  CoeHead F (M ≃ₛₗ[σ] M₂)

Full source

/-- Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence. -/
instance instCoeToSemilinearEquiv [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] : CoeHead F (M ≃ₛₗ[σ] M₂) where
  coe f := semilinearEquiv f

Canonical Semilinear Equivalence Interpretation from Class Element

Informal description

For any type `F` that forms a `SemilinearEquivClass` with ring homomorphisms $\sigma: R \to S$ and $\sigma': S \to R$ forming inverse pairs, and modules $M$ over $R$ and $M_2$ over $S$, there exists a canonical way to interpret any element $f \in F$ as a semilinear equivalence $M \simeq_{\sigma} M_2$. This equivalence is both an additive group isomorphism and satisfies the semilinearity property $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all $r \in R$ and $x \in M$.

LinearEquiv.instCoeLinearMap instance

: Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)

Full source

instance : Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂) :=
  ⟨toLinearMap⟩

Semilinear Equivalence as Semilinear Map

Informal description

Every semilinear equivalence $e: M \simeq_{\sigma} M_2$ can be viewed as a semilinear map $M \to_{\sigma} M_2$.

LinearEquiv.toEquiv definition

: (M ≃ₛₗ[σ] M₂) → M ≃ M₂

Full source

/-- The equivalence of types underlying a linear equivalence. -/
def toEquiv : (M ≃ₛₗ[σ] M₂) → M ≃ M₂ := fun f ↦ f.toAddEquiv.toEquiv

Underlying equivalence of a linear isomorphism

Informal description

Given a linear equivalence (semilinear isomorphism) $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, the function returns the underlying bijective map $M \simeq M_2$ between the additive commutative monoids.

LinearEquiv.toEquiv_injective theorem

: Function.Injective (toEquiv : (M ≃ₛₗ[σ] M₂) → M ≃ M₂)

Full source

theorem toEquiv_injective : Function.Injective (toEquiv : (M ≃ₛₗ[σ] M₂) → M ≃ M₂) :=
  fun ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ h ↦
    (LinearEquiv.mk.injEq _ _ _ _ _ _ _ _).mpr
      ⟨LinearMap.ext (congr_fun (Equiv.mk.inj h).1), (Equiv.mk.inj h).2⟩

Injectivity of the Underlying Equivalence Map for Semilinear Isomorphisms

Informal description

The function that extracts the underlying bijective map from a semilinear equivalence is injective. That is, for any two semilinear equivalences $e_1, e_2 : M \simeq_{\sigma} M_2$, if their underlying bijections are equal ($e_1.\text{toEquiv} = e_2.\text{toEquiv}$), then $e_1 = e_2$.

LinearEquiv.toEquiv_inj theorem

{e₁ e₂ : M ≃ₛₗ[σ] M₂} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

Full source

@[simp]
theorem toEquiv_inj {e₁ e₂ : M ≃ₛₗ[σ] M₂} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂ :=
  toEquiv_injective.eq_iff

Equality of Semilinear Isomorphisms via Underlying Bijections

Informal description

For any two semilinear equivalences $e_1, e_2 \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively (with respect to a ring homomorphism $\sigma \colon R \to S$), the underlying bijections $e_1.\text{toEquiv}$ and $e_2.\text{toEquiv}$ are equal if and only if $e_1 = e_2$.

LinearEquiv.toLinearMap_injective theorem

: Injective (toLinearMap : (M ≃ₛₗ[σ] M₂) → M →ₛₗ[σ] M₂)

Full source

theorem toLinearMap_injective : Injective (toLinearMap : (M ≃ₛₗ[σ] M₂) → M →ₛₗ[σ] M₂) :=
  fun _ _ H ↦ toEquiv_injective <| Equiv.ext <| LinearMap.congr_fun H

Injectivity of the Semilinear Map Extraction from Semilinear Equivalences

Informal description

The function that extracts the underlying semilinear map from a semilinear equivalence is injective. That is, for any two semilinear equivalences $e_1, e_2 : M \simeq_{\sigma} M_2$, if their underlying semilinear maps are equal ($e_1.\text{toLinearMap} = e_2.\text{toLinearMap}$), then $e_1 = e_2$.

LinearEquiv.toLinearMap_inj theorem

{e₁ e₂ : M ≃ₛₗ[σ] M₂} : (↑e₁ : M →ₛₗ[σ] M₂) = e₂ ↔ e₁ = e₂

Full source

@[simp, norm_cast]
theorem toLinearMap_inj {e₁ e₂ : M ≃ₛₗ[σ] M₂} : (↑e₁ : M →ₛₗ[σ] M₂) = e₂ ↔ e₁ = e₂ :=
  toLinearMap_injective.eq_iff

Equality of Semilinear Isomorphisms via Underlying Semilinear Maps

Informal description

For any two semilinear equivalences $e_1, e_2 \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively (with respect to a ring homomorphism $\sigma \colon R \to S$), the underlying semilinear maps $e_1$ and $e_2$ are equal if and only if $e_1 = e_2$.

LinearEquiv.instEquivLike instance

: EquivLike (M ≃ₛₗ[σ] M₂) M M₂

Full source

instance : EquivLike (M ≃ₛₗ[σ] M₂) M M₂ where
  coe e := e.toFun
  inv := LinearEquiv.invFun
  coe_injective' _ _ h _ := toLinearMap_injective (DFunLike.coe_injective h)
  left_inv := LinearEquiv.left_inv
  right_inv := LinearEquiv.right_inv

Bijective Nature of Semilinear Equivalences

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, the underlying map $e$ is an equivalence-like bijection between $M$ and $M_2$. This means that $e$ can be injectively coerced to a bijective function between the underlying types of $M$ and $M_2$.

LinearEquiv.instSemilinearEquivClass instance

: SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂

Full source

instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂ where
  map_add := (·.map_add')
  map_smulₛₗ := (·.map_smul')

Semilinear Equivalence Class of Module Isomorphisms

Informal description

The type of semilinear equivalences $M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, forms a class of semilinear equivalences. This means that any such equivalence is an additive bijection that satisfies the semilinearity condition $e(r \cdot x) = \sigma(r) \cdot e(x)$ for all $r \in R$ and $x \in M$.

LinearEquiv.toLinearMap_eq_coe theorem

{e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMapClass.semilinearMap e

Full source

theorem toLinearMap_eq_coe {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMapClass.semilinearMap e :=
  rfl

Equality of Underlying Linear Map and Coerced Semilinear Map in Linear Equivalence

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma \colon R \to S$, the underlying linear map $e.toLinearMap$ is equal to the semilinear map obtained by coercing $e$ to a function via `SemilinearMapClass.semilinearMap`.

LinearEquiv.coe_mk theorem

 {to_fun inv_fun map_add map_smul left_inv right_inv} :
  (⟨⟨⟨to_fun, map_add⟩, map_smul⟩, inv_fun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) = to_fun

Full source

@[simp]
theorem coe_mk {to_fun inv_fun map_add map_smul left_inv right_inv} :
    (⟨⟨⟨to_fun, map_add⟩, map_smul⟩, inv_fun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) = to_fun := rfl

Underlying Function of Semilinear Equivalence Construction

Informal description

Given a semilinear equivalence $e : M \simeq_{\sigma} M_2$ constructed from: - A function $to\_fun : M \to M_2$, - An inverse function $inv\_fun : M_2 \to M$, - Proofs that $to\_fun$ is additive ($map\_add$) and semilinear with respect to $\sigma$ ($map\_smul$), - Proofs that $inv\_fun$ is a left inverse ($left\_inv$) and right inverse ($right\_inv$) of $to\_fun$, then the underlying function of $e$ is equal to $to\_fun$.

LinearEquiv.coe_injective theorem

: @Injective (M ≃ₛₗ[σ] M₂) (M → M₂) CoeFun.coe

Full source

theorem coe_injective : @Injective (M ≃ₛₗ[σ] M₂) (M → M₂) CoeFun.coe :=
  DFunLike.coe_injective

Injectivity of Coercion for Semilinear Equivalences

Informal description

The canonical coercion from the type of semilinear equivalences $M \simeq_{\sigma} M_2$ to the type of functions $M \to M_2$ is injective. That is, if two semilinear equivalences $e_1, e_2 : M \simeq_{\sigma} M_2$ satisfy $e_1(x) = e_2(x)$ for all $x \in M$, then $e_1 = e_2$.

LinearEquiv.coe_coe theorem

: ⇑(e : M →ₛₗ[σ] M₂) = e

Full source

@[simp, norm_cast]
theorem coe_coe : ⇑(e : M →ₛₗ[σ] M₂) = e :=
  rfl

Coercion of Semilinear Equivalence to Semilinear Map Preserves Function

Informal description

For a semilinear equivalence $e : M \simeq_{\sigma} M_2$, the underlying function of $e$ viewed as a semilinear map (via coercion) is equal to $e$ itself.

LinearEquiv.coe_toEquiv theorem

: ⇑(e.toEquiv) = e

Full source

@[simp]
theorem coe_toEquiv : ⇑(e.toEquiv) = e :=
  rfl

Equality of Underlying Equivalence and Semilinear Equivalence Functions

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, the underlying function of the associated equivalence $e.\text{toEquiv}$ is equal to $e$ itself.

LinearEquiv.coe_toLinearMap theorem

: ⇑e.toLinearMap = e

Full source

@[simp]
theorem coe_toLinearMap : ⇑e.toLinearMap = e :=
  rfl

Equality of Linear Map and Semilinear Equivalence Functions

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, the underlying function of the associated linear map $e.toLinearMap$ is equal to $e$ itself.

LinearEquiv.toFun_eq_coe theorem

: e.toFun = e

Full source

theorem toFun_eq_coe : e.toFun = e := by dsimp

Underlying Function of Semilinear Equivalence Equals Itself

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$, the underlying function of $e$ is equal to $e$ itself, i.e., $e.\text{toFun} = e$.

LinearEquiv.ext theorem

(h : ∀ x, e x = e' x) : e = e'

Full source

@[ext]
theorem ext (h : ∀ x, e x = e' x) : e = e' :=
  DFunLike.ext _ _ h

Extensionality of Semilinear Equivalences

Informal description

For any two semilinear equivalences $e, e' : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, if $e(x) = e'(x)$ for all $x \in M$, then $e = e'$.

LinearEquiv.congr_arg theorem

{x x'} : x = x' → e x = e x'

Full source

protected theorem congr_arg {x x'} : x = x' → e x = e x' :=
  DFunLike.congr_arg e

Semilinear equivalence preserves equality: $x = x' \implies e(x) = e(x')$

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ and any elements $x, x' \in M$, if $x = x'$, then $e(x) = e(x')$.

LinearEquiv.congr_fun theorem

(h : e = e') (x : M) : e x = e' x

Full source

protected theorem congr_fun (h : e = e') (x : M) : e x = e' x :=
  DFunLike.congr_fun h x

Pointwise Equality of Semilinear Equivalences

Informal description

For any two semilinear equivalences $e, e' : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, if $e = e'$, then $e(x) = e'(x)$ for all $x \in M$.

LinearEquiv.refl definition

[Module R M] : M ≃ₗ[R] M

Full source

/-- The identity map is a linear equivalence. -/
@[refl]
def refl [Module R M] : M ≃ₗ[R] M :=
  { LinearMap.id, Equiv.refl M with }

Identity linear equivalence

Informal description

The identity map on a module $M$ over a semiring $R$ is a linear equivalence, i.e., it is a bijective linear map from $M$ to itself that preserves the module structure.

LinearEquiv.refl_apply theorem

[Module R M] (x : M) : refl R M x = x

Full source

@[simp]
theorem refl_apply [Module R M] (x : M) : refl R M x = x :=
  rfl

Identity Linear Equivalence Acts as Identity on Elements

Informal description

For any module $M$ over a semiring $R$ and any element $x \in M$, the identity linear equivalence $\text{refl}_R M$ applied to $x$ equals $x$ itself, i.e., $(\text{refl}_R M)(x) = x$.

LinearEquiv.symm definition

(e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M

Full source

/-- Linear equivalences are symmetric. -/
@[symm]
def symm (e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M :=
  { e.toLinearMap.inverse e.invFun e.left_inv e.right_inv,
    e.toEquiv.symm with
    toFun := e.toLinearMap.inverse e.invFun e.left_inv e.right_inv
    invFun := e.toEquiv.symm.invFun
    map_smul' := fun r x ↦ by rw [map_smulₛₗ] }

Inverse of a semilinear equivalence

Informal description

Given a semilinear equivalence $ e : M \simeq_{\sigma} M_2 $ between modules $ M $ and $ M_2 $ over semirings $ R $ and $ S $ respectively, with respect to a ring homomorphism $ \sigma: R \to S $, the inverse equivalence $ e^{-1} : M_2 \simeq_{\sigma'} M $ is defined, where $ \sigma': S \to R $ is the inverse ring homomorphism of $ \sigma $. The inverse equivalence satisfies $ e^{-1}(s \cdot y) = \sigma'(s) \cdot e^{-1}(y) $ for all $ s \in S $ and $ y \in M_2 $, and it is both a left and right inverse of $ e $.

LinearEquiv.Simps.apply definition

 {R : Type*} {S : Type*} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ']
  [RingHomInvPair σ' σ] {M : Type*} {M₂ : Type*} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
  (e : M ≃ₛₗ[σ] M₂) : M → M₂

Full source

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type*} {S : Type*} [Semiring R] [Semiring S]
    {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    {M : Type*} {M₂ : Type*} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
    (e : M ≃ₛₗ[σ] M₂) : M → M₂ :=
  e

Application of a semilinear equivalence

Informal description

Given semirings $R$ and $S$, a ring homomorphism $\sigma: R \to S$ and its inverse pair $\sigma': S \to R$ satisfying compatibility conditions, additive commutative monoids $M$ and $M_2$ with module structures over $R$ and $S$ respectively, and a semilinear equivalence $e: M \simeq_{\sigma} M_2$, the function `apply` maps an element $x \in M$ to its image $e(x) \in M_2$.

LinearEquiv.Simps.symm_apply definition

 {R : Type*} {S : Type*} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ']
  [RingHomInvPair σ' σ] {M : Type*} {M₂ : Type*} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
  (e : M ≃ₛₗ[σ] M₂) : M₂ → M

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} {S : Type*} [Semiring R] [Semiring S]
    {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    {M : Type*} {M₂ : Type*} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
    (e : M ≃ₛₗ[σ] M₂) : M₂ → M :=
  e.symm

Preimage under semilinear equivalence

Informal description

Given a semilinear equivalence $ e : M \simeq_{\sigma} M_2 $ between modules $ M $ and $ M_2 $ over semirings $ R $ and $ S $ respectively, with respect to a ring homomorphism $ \sigma: R \to S $, the function maps an element $ y \in M_2 $ to its preimage $ e^{-1}(y) \in M $ under the inverse equivalence $ e^{-1} $.

LinearEquiv.invFun_eq_symm theorem

: e.invFun = e.symm

Full source

@[simp]
theorem invFun_eq_symm : e.invFun = e.symm :=
  rfl

Inverse Function of Semilinear Equivalence Equals Its Symmetric Counterpart

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, the inverse function of $e$ is equal to its inverse semilinear equivalence $e^{-1} : M_2 \simeq_{\sigma'} M$, i.e., $e^{-1} = e^{-1}$.

LinearEquiv.coe_toEquiv_symm theorem

: e.toEquiv.symm = e.symm

Full source

@[simp]
theorem coe_toEquiv_symm : e.toEquiv.symm = e.symm :=
  rfl

Equality of Inverse Bijection and Inverse Semilinear Equivalence

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$, the inverse of the underlying bijection $e.toEquiv.symm$ is equal to the inverse semilinear equivalence $e.symm$.

LinearEquiv.trans definition

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
  M₁ ≃ₛₗ[σ₁₃] M₃

Full source

/-- Linear equivalences are transitive. -/
-- Note: the `RingHomCompTriple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
-- implicitly for lemmas like `LinearEquiv.self_trans_symm`.
@[trans, nolint unusedArguments]
def trans
    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
    {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂}
    [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
    {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃]
    (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : M₁ ≃ₛₗ[σ₁₃] M₃ :=
  { e₂₃.toLinearMap.comp e₁₂.toLinearMap, e₁₂.toEquiv.trans e₂₃.toEquiv with }

Composition of linear equivalences

Informal description

Given three modules $M₁$, $M₂$, and $M₃$ over semirings $R₁$, $R₂$, and $R₃$ respectively, and ring homomorphisms $\sigma_{12}: R₁ \to R₂$, $\sigma_{23}: R₂ \to R₃$, $\sigma_{32}: R₃ \to R₂$, $\sigma_{21}: R₂ \to R₁$ satisfying the compatibility conditions `RingHomInvPair` and `RingHomCompTriple`, the composition of two linear equivalences $e_{12}: M₁ \simeq_{\sigma_{12}} M₂$ and $e_{23}: M₂ \simeq_{\sigma_{23}} M₃$ forms a linear equivalence $M₁ \simeq_{\sigma_{13}} M₃$, where $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$.

LinearEquiv.transNotation definition

: Lean.TrailingParserDescr✝

Full source

/-- `e₁ ≪≫ₗ e₂` denotes the composition of the linear equivalences `e₁` and `e₂`. -/
notation3:80 (name := transNotation) e₁:80 " ≪≫ₗ " e₂:81 =>
  @LinearEquiv.trans _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _)
    (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids RingHomCompTriple.ids
    RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids
    RingHomInvPair.ids e₁ e₂

Composition of linear equivalences

Informal description

The notation `e₁ ≪≫ₗ e₂` denotes the composition of two linear equivalences `e₁` and `e₂`, where both equivalences are linear over the same ring (using the identity ring homomorphism).

LinearEquiv.transNotation.delab_app.LinearEquiv.trans definition

: Delab✝

Full source

/-- `e₁ ≪≫ₗ e₂` denotes the composition of the linear equivalences `e₁` and `e₂`. -/
notation3:80 (name := transNotation) e₁:80 " ≪≫ₗ " e₂:81 =>
  @LinearEquiv.trans _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _)
    (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids RingHomCompTriple.ids
    RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids
    RingHomInvPair.ids e₁ e₂

Composition of linear equivalences

Informal description

The notation `e₁ ≪≫ₗ e₂` denotes the composition of two linear equivalences `e₁` and `e₂`, where both equivalences are linear over the same ring (using the identity ring homomorphism).

LinearEquiv.coe_toAddEquiv theorem

: e.toAddEquiv = e

Full source

@[simp]
theorem coe_toAddEquiv : e.toAddEquiv = e :=
  rfl

Underlying Additive Equivalence of a Linear Equivalence is Itself

Informal description

For any linear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, the underlying additive equivalence of $e$ is equal to $e$ itself.

LinearEquiv.coe_addEquiv_apply theorem

(x : M) : (e : M ≃+ M₂) x = e x

Full source

@[simp]
lemma coe_addEquiv_apply (x : M) : (e : M ≃+ M₂) x = e x := by
  rfl

Additive Equivalence Application Coincides with Linear Equivalence Application

Informal description

For any linear equivalence $e : M \simeq M_2$ between modules $M$ and $M_2$, and for any element $x \in M$, the application of $e$ as an additive equivalence to $x$ is equal to the application of $e$ itself to $x$, i.e., $(e : M \simeq^+ M_2)(x) = e(x)$.

LinearEquiv.toAddMonoidHom_commutes theorem

: e.toLinearMap.toAddMonoidHom = e.toAddEquiv.toAddMonoidHom

Full source

/-- The two paths coercion can take to an `AddMonoidHom` are equivalent -/
theorem toAddMonoidHom_commutes : e.toLinearMap.toAddMonoidHom = e.toAddEquiv.toAddMonoidHom :=
  rfl

Commutativity of Additive Monoid Homomorphism Paths for Linear Equivalences

Informal description

For any linear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$, the additive monoid homomorphism obtained from the underlying linear map of $e$ is equal to the additive monoid homomorphism obtained from the underlying additive equivalence of $e$. In other words, the diagram commutes when converting $e$ to an `AddMonoidHom` through either path.

LinearEquiv.coe_toAddEquiv_symm theorem

: (e₁₂.symm : M₂ ≃+ M₁) = (e₁₂ : M₁ ≃+ M₂).symm

Full source

lemma coe_toAddEquiv_symm : (e₁₂.symm : M₂ ≃+ M₁) = (e₁₂ : M₁ ≃+ M₂).symm := by
  rfl

Inverse of Linear Equivalence as Additive Equivalence

Informal description

For any linear equivalence $e_{12} : M_1 \simeq^+ M_2$ between additive commutative monoids $M_1$ and $M_2$, the underlying additive equivalence of the inverse $e_{12}^{-1} : M_2 \simeq^+ M_1$ is equal to the inverse of the underlying additive equivalence of $e_{12}$.

LinearEquiv.trans_apply theorem

(c : M₁) : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃) c = e₂₃ (e₁₂ c)

Full source

@[simp]
theorem trans_apply (c : M₁) : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃) c = e₂₃ (e₁₂ c) :=
  rfl

Composition of Linear Equivalences Preserves Application

Informal description

For any element $c \in M_1$, the composition of two linear equivalences $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and $e_{23}: M_2 \simeq_{\sigma_{23}} M_3$ evaluated at $c$ equals the application of $e_{23}$ to the result of applying $e_{12}$ to $c$, i.e., $$(e_{12} \circ e_{23})(c) = e_{23}(e_{12}(c)).$$

LinearEquiv.coe_trans theorem

 : (e₁₂.trans e₂₃ : M₁ →ₛₗ[σ₁₃] M₃) = (e₂₃ : M₂ →ₛₗ[σ₂₃] M₃).comp (e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)

Full source

theorem coe_trans :
    (e₁₂.trans e₂₃ : M₁ →ₛₗ[σ₁₃] M₃) = (e₂₃ : M₂ →ₛₗ[σ₂₃] M₃).comp (e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) :=
  rfl

Composition of Linear Equivalences as Semilinear Maps

Informal description

Let $M₁$, $M₂$, and $M₃$ be modules over semirings $R₁$, $R₂$, and $R₃$ respectively, with ring homomorphisms $\sigma_{12}: R₁ \to R₂$, $\sigma_{23}: R₂ \to R₃$, and $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Given linear equivalences $e_{12}: M₁ \simeq_{\sigma_{12}} M₂$ and $e_{23}: M₂ \simeq_{\sigma_{23}} M₃$, the underlying semilinear map of their composition $e_{12} \circ e_{23}: M₁ \simeq_{\sigma_{13}} M₃$ is equal to the composition of the underlying semilinear maps, i.e., $(e_{12} \circ e_{23}) = e_{23} \circ e_{12}$ as maps from $M₁$ to $M₃$.

LinearEquiv.apply_symm_apply theorem

(c : M₂) : e (e.symm c) = c

Full source

@[simp]
theorem apply_symm_apply (c : M₂) : e (e.symm c) = c :=
  e.right_inv c

Inverse Image Application Identity for Semilinear Equivalences

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ and any element $c \in M_2$, applying $e$ to the inverse image $e^{-1}(c)$ yields $c$ again, i.e., $e(e^{-1}(c)) = c$.

LinearEquiv.symm_apply_apply theorem

(b : M) : e.symm (e b) = b

Full source

@[simp]
theorem symm_apply_apply (b : M) : e.symm (e b) = b :=
  e.left_inv b

Inverse Semilinear Equivalence Preserves Application: $e^{-1}(e(b)) = b$

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, and for any element $b \in M$, the inverse equivalence $e^{-1}$ satisfies $e^{-1}(e(b)) = b$.

LinearEquiv.trans_symm theorem

: (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm = e₂₃.symm.trans e₁₂.symm

Full source

@[simp]
theorem trans_symm : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm = e₂₃.symm.trans e₁₂.symm :=
  rfl

Inverse of Composition of Linear Equivalences is Reverse Composition of Inverses

Informal description

Given linear equivalences $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and $e_{23}: M_2 \simeq_{\sigma_{23}} M_3$ between modules over semirings with compatible ring homomorphisms $\sigma_{12}: R_1 \to R_2$, $\sigma_{23}: R_2 \to R_3$, the inverse of their composition $(e_{12} \circ e_{23})^{-1}$ is equal to the composition of their inverses in reverse order, i.e., $e_{23}^{-1} \circ e_{12}^{-1}$.

LinearEquiv.symm_trans_apply theorem

(c : M₃) : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm c = e₁₂.symm (e₂₃.symm c)

Full source

theorem symm_trans_apply (c : M₃) :
    (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm c = e₁₂.symm (e₂₃.symm c) :=
  rfl

Inverse of Composition of Linear Equivalences Applied to Element

Informal description

For any element $c \in M_3$, the inverse of the composition of two linear equivalences $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and $e_{23}: M_2 \simeq_{\sigma_{23}} M_3$ applied to $c$ equals the composition of their inverses applied to $c$, i.e., $$(e_{12} \circ e_{23})^{-1}(c) = e_{12}^{-1}(e_{23}^{-1}(c)).$$

LinearEquiv.trans_refl theorem

: e.trans (refl S M₂) = e

Full source

@[simp]
theorem trans_refl : e.trans (refl S M₂) = e :=
  toEquiv_injective e.toEquiv.trans_refl

Right Identity Law for Composition of Linear Equivalences

Informal description

For any linear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma \colon R \to S$, the composition of $e$ with the identity linear equivalence on $M_2$ equals $e$ itself, i.e., $e \circ \text{id}_{M_2} = e$.

LinearEquiv.refl_trans theorem

: (refl R M).trans e = e

Full source

@[simp]
theorem refl_trans : (refl R M).trans e = e :=
  toEquiv_injective e.toEquiv.refl_trans

Identity Linear Equivalence is Left Neutral for Composition

Informal description

For any module $M$ over a semiring $R$ and any linear equivalence $e \colon M \simeq_{\sigma} M_2$, the composition of the identity linear equivalence on $M$ with $e$ is equal to $e$ itself, i.e., $$(\text{refl}_R M) \circ e = e.$$

LinearEquiv.symm_apply_eq theorem

{x y} : e.symm x = y ↔ x = e y

Full source

theorem symm_apply_eq {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

Characterization of the Inverse of a Semilinear Equivalence: $e^{-1}(x) = y \leftrightarrow x = e(y)$

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma \colon R \to S$, and for any elements $x \in M_2$ and $y \in M$, the equality $e^{-1}(x) = y$ holds if and only if $x = e(y)$.

LinearEquiv.comp_symm_eq theorem

{α : Type*} (f : M₂ → α) (g : M₁ → α) : g ∘ e₁₂.symm = f ↔ g = f ∘ e₁₂

Full source

theorem comp_symm_eq {α : Type*} (f : M₂ → α) (g : M₁ → α) : g ∘ e₁₂.symmg ∘ e₁₂.symm = f ↔ g = f ∘ e₁₂ :=
  e₁₂.toEquiv.comp_symm_eq f g

Composition with Inverse Semilinear Equivalence Condition: $g \circ e^{-1} = f \leftrightarrow g = f \circ e$

Informal description

Let $M_1$ and $M_2$ be modules over semirings $R$ and $S$ respectively, and let $e_{12}: M_1 \simeq_{\sigma} M_2$ be a semilinear equivalence with respect to a ring homomorphism $\sigma: R \to S$. For any type $\alpha$ and functions $f: M_2 \to \alpha$ and $g: M_1 \to \alpha$, the composition $g \circ e_{12}^{-1}$ equals $f$ if and only if $g$ equals $f \circ e_{12}$.

LinearEquiv.symm_comp_eq theorem

{α : Type*} (f : α → M₁) (g : α → M₂) : e₁₂.symm ∘ g = f ↔ g = e₁₂ ∘ f

Full source

theorem symm_comp_eq {α : Type*} (f : α → M₁) (g : α → M₂) : e₁₂.symm ∘ ge₁₂.symm ∘ g = f ↔ g = e₁₂ ∘ f :=
  e₁₂.toEquiv.symm_comp_eq f g

Characterization of Composition with Inverse Linear Equivalence: $e^{-1} \circ g = f \leftrightarrow g = e \circ f$

Informal description

Let $M_1$ and $M_2$ be modules over semirings $R$ and $S$ respectively, and let $e_{12} : M_1 \simeq_{\sigma} M_2$ be a linear equivalence with respect to a ring homomorphism $\sigma: R \to S$. For any type $\alpha$ and functions $f : \alpha \to M_1$, $g : \alpha \to M_2$, the composition $e_{12}^{-1} \circ g$ equals $f$ if and only if $g$ equals $e_{12} \circ f$.

LinearEquiv.comp_toLinearMap_symm_eq theorem

 (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) : g.comp e₁₂.symm.toLinearMap = f ↔ g = f.comp e₁₂.toLinearMap

Full source

theorem comp_toLinearMap_symm_eq (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
    g.comp e₁₂.symm.toLinearMap = f ↔ g = f.comp e₁₂.toLinearMap := by
  constructor <;> intro H <;> ext
  · simp [← H, ← e₁₂.toEquiv.comp_symm_eq f g]
  · simp [H, e₁₂.toEquiv.comp_symm_eq f g]

Composition with Inverse Linear Equivalence: $g \circ e^{-1} = f \leftrightarrow g = f \circ e$

Informal description

Let $M_1$, $M_2$, and $M_3$ be modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12}: R \to S$, $\sigma_{23}: S \to T$, and $\sigma_{13}: R \to T$ such that $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Given a linear equivalence $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and semilinear maps $f: M_2 \to_{\sigma_{23}} M_3$ and $g: M_1 \to_{\sigma_{13}} M_3$, the composition $g \circ e_{12}^{-1}$ equals $f$ if and only if $g$ equals $f \circ e_{12}$.

LinearEquiv.toLinearMap_symm_comp_eq theorem

 (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) : e₁₂.symm.toLinearMap.comp g = f ↔ g = e₁₂.toLinearMap.comp f

Full source

theorem toLinearMap_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
    e₁₂.symm.toLinearMap.comp g = f ↔ g = e₁₂.toLinearMap.comp f := by
  constructor <;> intro H <;> ext
  · simp [← H, ← e₁₂.toEquiv.symm_comp_eq f g]
  · simp [H, e₁₂.toEquiv.symm_comp_eq f g]

Equivalence of Composition with Inverse Linear Map

Informal description

Let $R$, $S$ be semirings with ring homomorphisms $\sigma_{31}: R \to S$ and $\sigma_{32}: S \to R$ forming inverse pairs. Let $M_1$, $M_2$ be modules over $R$, $S$ respectively, and $M_3$ a module over $R$. Given a linear equivalence $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and semilinear maps $f: M_3 \to_{\sigma_{31}} M_1$, $g: M_3 \to_{\sigma_{32}} M_2$, the following equivalence holds: \[ e_{12}^{-1} \circ g = f \quad \text{if and only if} \quad g = e_{12} \circ f \] where $\circ$ denotes composition of linear maps and $e_{12}^{-1}$ is the inverse linear equivalence of $e_{12}$.

LinearEquiv.comp_toLinearMap_eq_iff theorem

(f g : M₃ →ₛₗ[σ₃₁] M₁) : e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g

Full source

@[simp]
theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) :
    e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g := by
  refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
  rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]

Linear Equivalence Preserves Distinctness Under Composition

Informal description

Let $R$ and $S$ be semirings with ring homomorphisms $\sigma_{12}: R \to S$ and $\sigma_{21}: S \to R$ forming inverse pairs. Let $M_1$ be a module over $R$, $M_2$ a module over $S$, and $M_3$ a module over $R$. Given a linear equivalence $e_{12}: M_1 \simeq_{\sigma_{12}} M_2$ and semilinear maps $f, g: M_3 \to_{\sigma_{31}} M_1$, the following equivalence holds: \[ e_{12} \circ f = e_{12} \circ g \quad \text{if and only if} \quad f = g \] where $\circ$ denotes composition of linear maps.

LinearEquiv.refl_symm theorem

[Module R M] : (refl R M).symm = LinearEquiv.refl R M

Full source

@[simp]
theorem refl_symm [Module R M] : (refl R M).symm = LinearEquiv.refl R M :=
  rfl

Inverse of Identity Linear Equivalence is Itself

Informal description

For any module $M$ over a semiring $R$, the inverse of the identity linear equivalence $\text{refl}_R M$ is equal to itself, i.e., $(\text{refl}_R M)^{-1} = \text{refl}_R M$.

LinearEquiv.self_trans_symm theorem

(f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.trans f.symm = LinearEquiv.refl R₁ M₁

Full source

@[simp]
theorem self_trans_symm (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.trans f.symm = LinearEquiv.refl R₁ M₁ := by
  ext x
  simp

Composition of Semilinear Equivalence with Its Inverse Yields Identity

Informal description

For any semilinear equivalence $f : M_1 \simeq_{\sigma_{12}} M_2$ between modules $M_1$ and $M_2$ over semirings $R_1$ and $R_2$ respectively, with respect to a ring homomorphism $\sigma_{12}: R_1 \to R_2$, the composition of $f$ with its inverse $f^{-1}$ is equal to the identity linear equivalence on $M_1$, i.e., $f \circ f^{-1} = \text{id}_{M_1}$.

LinearEquiv.symm_trans_self theorem

(f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.symm.trans f = LinearEquiv.refl R₂ M₂

Full source

@[simp]
theorem symm_trans_self (f : M₁ ≃ₛₗ[σ₁₂] M₂) : f.symm.trans f = LinearEquiv.refl R₂ M₂ := by
  ext x
  simp

Inverse Composition Yields Identity: $f^{-1} \circ f = \text{id}_{M_2}$

Informal description

For any semilinear equivalence $f \colon M_1 \simeq_{\sigma_{12}} M_2$ between modules $M_1$ and $M_2$ over semirings $R_1$ and $R_2$ respectively, the composition of the inverse equivalence $f^{-1}$ with $f$ is equal to the identity linear equivalence on $M_2$. That is, \[ f^{-1} \circ f = \text{id}_{M_2}, \] where $\text{id}_{M_2}$ denotes the identity linear equivalence on $M_2$.

LinearEquiv.refl_toLinearMap theorem

[Module R M] : (LinearEquiv.refl R M : M →ₗ[R] M) = LinearMap.id

Full source

@[simp]
theorem refl_toLinearMap [Module R M] : (LinearEquiv.refl R M : M →ₗ[R] M) = LinearMap.id :=
  rfl

Identity Linear Equivalence as Identity Map

Informal description

For a module $M$ over a semiring $R$, the underlying linear map of the identity linear equivalence $\text{refl}_R M$ is equal to the identity linear map $\text{id}_R$ on $M$.

LinearEquiv.comp_coe theorem

 [Module R M] [Module R M₂] [Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
  (f' : M₂ →ₗ[R] M₃).comp (f : M →ₗ[R] M₂) = (f.trans f' : M ≃ₗ[R] M₃)

Full source

@[simp]
theorem comp_coe [Module R M] [Module R M₂] [Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
    (f' : M₂ →ₗ[R] M₃).comp (f : M →ₗ[R] M₂) = (f.trans f' : M ≃ₗ[R] M₃) :=
  rfl

Composition of Linear Maps Underlying Linear Equivalences

Informal description

Let $M$, $M_2$, and $M_3$ be modules over a semiring $R$, and let $f: M \simeq_{R} M_2$ and $f': M_2 \simeq_{R} M_3$ be linear equivalences. Then the composition of the underlying linear maps $f' \circ f$ equals the linear map underlying the composed equivalence $f' \circ f$. In symbols: \[ (f' \colon M_2 \to_{R} M_3) \circ (f \colon M \to_{R} M_2) = (f' \circ f \colon M \simeq_{R} M_3) \]

LinearEquiv.mk_coe theorem

(f h₁ h₂) : (LinearEquiv.mk e f h₁ h₂ : M ≃ₛₗ[σ] M₂) = e

Full source

@[simp]
theorem mk_coe (f h₁ h₂) : (LinearEquiv.mk e f h₁ h₂ : M ≃ₛₗ[σ] M₂) = e :=
  ext fun _ ↦ rfl

Construction of Semilinear Equivalence Preserves Underlying Map

Informal description

Given a semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, and given functions $f : M_2 \to M$, $h_1 : \text{LeftInverse}\ f\ e$, and $h_2 : \text{RightInverse}\ f\ e$, the constructed linear equivalence $\text{mk}\ e\ f\ h_1\ h_2$ is equal to $e$ when viewed as a function.

LinearEquiv.map_add theorem

(a b : M) : e (a + b) = e a + e b

Full source

protected theorem map_add (a b : M) : e (a + b) = e a + e b :=
  map_add e a b

Additivity of Semilinear Equivalences

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, and for any elements $a, b \in M$, the map $e$ preserves addition: \[ e(a + b) = e(a) + e(b). \]

LinearEquiv.map_zero theorem

: e 0 = 0

Full source

protected theorem map_zero : e 0 = 0 :=
  map_zero e

Semilinear Equivalence Preserves Zero

Informal description

For any semilinear equivalence $e: M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, the map $e$ preserves the zero element, i.e., $e(0) = 0$.

LinearEquiv.map_smulₛₗ theorem

(c : R) (x : M) : e (c • x) = (σ : R → S) c • e x

Full source

protected theorem map_smulₛₗ (c : R) (x : M) : e (c • x) = (σ : R → S) c • e x :=
  e.map_smul' c x

Semilinear Equivalence Preserves Scalar Multiplication: $e(c \cdot x) = \sigma(c) \cdot e(x)$

Informal description

Let $R$ and $S$ be semirings, $\sigma: R \to S$ a ring homomorphism, and $M$, $M_2$ be modules over $R$ and $S$ respectively. For any semilinear equivalence $e: M \simeq_{\sigma} M_2$ and any scalar $c \in R$ and element $x \in M$, we have: \[ e(c \cdot x) = \sigma(c) \cdot e(x) \]

LinearEquiv.map_smul theorem

(e : N₁ ≃ₗ[R₁] N₂) (c : R₁) (x : N₁) : e (c • x) = c • e x

Full source

theorem map_smul (e : N₁ ≃ₗ[R₁] N₂) (c : R₁) (x : N₁) : e (c • x) = c • e x :=
  map_smulₛₗ e c x

Linear Equivalence Preserves Scalar Multiplication: $e(c \cdot x) = c \cdot e(x)$

Informal description

Let $R_1$ be a semiring and $N_1$, $N_2$ be modules over $R_1$. For any linear equivalence $e: N_1 \simeq_{R_1} N_2$ (where $\sigma = \text{id}_{R_1}$), scalar $c \in R_1$, and element $x \in N_1$, we have: \[ e(c \cdot x) = c \cdot e(x) \]

LinearEquiv.map_eq_zero_iff theorem

{x : M} : e x = 0 ↔ x = 0

Full source

theorem map_eq_zero_iff {x : M} : e x = 0 ↔ x = 0 :=
  e.toAddEquiv.map_eq_zero_iff

Semilinear equivalence preserves zero: $e(x) = 0 \leftrightarrow x = 0$

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, and for any element $x \in M$, we have $e(x) = 0$ if and only if $x = 0$.

LinearEquiv.map_ne_zero_iff theorem

{x : M} : e x ≠ 0 ↔ x ≠ 0

Full source

theorem map_ne_zero_iff {x : M} : e x ≠ 0e x ≠ 0 ↔ x ≠ 0 :=
  e.toAddEquiv.map_ne_zero_iff

Nonzero Preservation under Semilinear Equivalence: $e(x) \neq 0 \leftrightarrow x \neq 0$

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, and for any element $x \in M$, we have $e(x) \neq 0$ if and only if $x \neq 0$.

LinearEquiv.symm_symm theorem

(e : M ≃ₛₗ[σ] M₂) : e.symm.symm = e

Full source

@[simp]
theorem symm_symm (e : M ≃ₛₗ[σ] M₂) : e.symm.symm = e := rfl

Double Inverse Property of Semilinear Equivalences

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma \colon R \to S$, the double inverse $e^{-1}$ of $e$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

LinearEquiv.symm_bijective theorem

 [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] :
  Function.Bijective (symm : (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M)

Full source

theorem symm_bijective [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] :
    Function.Bijective (symm : (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Map for Semilinear Equivalences

Informal description

Let $R$ and $S$ be semirings, $\sigma: R \to S$ and $\sigma': S \to R$ be ring homomorphisms forming inverse pairs, and $M$, $M_2$ be modules over $R$ and $S$ respectively. Then the inverse map $\text{symm} : (M \simeq_{\sigma} M_2) \to (M_2 \simeq_{\sigma'} M)$, which sends each semilinear equivalence to its inverse, is bijective.

LinearEquiv.mk_coe' theorem

(f h₁ h₂ h₃ h₄) : (LinearEquiv.mk ⟨⟨f, h₁⟩, h₂⟩ (⇑e) h₃ h₄ : M₂ ≃ₛₗ[σ'] M) = e.symm

Full source

@[simp]
theorem mk_coe' (f h₁ h₂ h₃ h₄) :
    (LinearEquiv.mk ⟨⟨f, h₁⟩, h₂⟩ (⇑e) h₃ h₄ : M₂ ≃ₛₗ[σ'] M) = e.symm :=
  symm_bijective.injective <| ext fun _ ↦ rfl

Constructed Semilinear Equivalence Equals Inverse

Informal description

Let $M$ and $M_2$ be modules over semirings $R$ and $S$ respectively, with ring homomorphisms $\sigma: R \to S$ and $\sigma': S \to R$ forming inverse pairs. Given functions $f: M_2 \to M$ and $e: M \to M_2$ satisfying: 1. $h_1$: $f$ is additive, 2. $h_2$: $f$ is semilinear with respect to $\sigma'$, 3. $h_3$: $f$ is a left inverse of $e$, 4. $h_4$: $f$ is a right inverse of $e$, then the constructed semilinear equivalence $\text{LinearEquiv.mk} \langle \langle f, h_1 \rangle, h_2 \rangle \, e \, h_3 \, h_4$ from $M_2$ to $M$ is equal to the inverse $e^{-1}$ of $e$.

LinearEquiv.symm_mk.aux definition

(f h₁ h₂ h₃ h₄)

Full source

/-- Auxiliary definition to avoid looping in `dsimp` with `LinearEquiv.symm_mk`. -/
protected def symm_mk.aux (f h₁ h₂ h₃ h₄) := (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm

Auxiliary construction for inverse semilinear equivalence

Informal description

The auxiliary function used in the construction of the inverse of a semilinear equivalence, ensuring that the definition of the inverse does not cause infinite loops during simplification.

LinearEquiv.symm_mk theorem

 (f h₁ h₂ h₃ h₄) :
  (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm =
    { symm_mk.aux e f h₁ h₂ h₃ h₄ with
      toFun := f
      invFun := e }

Full source

@[simp]
theorem symm_mk (f h₁ h₂ h₃ h₄) :
    (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm =
      { symm_mk.aux e f h₁ h₂ h₃ h₄ with
        toFun := f
        invFun := e } :=
  rfl

Inverse of Constructed Semilinear Equivalence

Informal description

Given a semilinear equivalence $e : M \simeq_{\sigma} M_2$ constructed from functions $e : M \to M_2$ and $f : M_2 \to M$ with properties $h_1$ (additivity), $h_2$ (semilinearity), $h_3$ (left inverse), and $h_4$ (right inverse), the inverse equivalence $e^{-1} : M_2 \simeq_{\sigma'} M$ is equal to the semilinear equivalence constructed from $f$ and $e$ with the same properties, where $\sigma'$ is the inverse ring homomorphism of $\sigma$.

LinearEquiv.coe_symm_mk theorem

 [Module R M] [Module R M₂] {to_fun inv_fun map_add map_smul left_inv right_inv} :
  ⇑(⟨⟨⟨to_fun, map_add⟩, map_smul⟩, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂).symm = inv_fun

Full source

@[simp]
theorem coe_symm_mk [Module R M] [Module R M₂]
    {to_fun inv_fun map_add map_smul left_inv right_inv} :
    ⇑(⟨⟨⟨to_fun, map_add⟩, map_smul⟩, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂).symm = inv_fun :=
  rfl

Inverse of Constructed Linear Equivalence is Given Inverse Function

Informal description

Let $M$ and $M_2$ be modules over a semiring $R$, and let $e : M \simeq_{\sigma} M_2$ be a linear equivalence constructed from functions $to\_fun : M \to M_2$, $inv\_fun : M_2 \to M$, with properties $map\_add$, $map\_smul$, $left\_inv$, and $right\_inv$. Then the underlying function of the inverse equivalence $e^{-1}$ is equal to $inv\_fun$.

LinearEquiv.bijective theorem

: Function.Bijective e

Full source

protected theorem bijective : Function.Bijective e :=
  e.toEquiv.bijective

Bijectivity of Semilinear Equivalences

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively (with respect to a ring homomorphism $\sigma: R \to S$), the underlying map $e : M \to M_2$ is bijective. That is, $e$ is both injective and surjective.

LinearEquiv.injective theorem

: Function.Injective e

Full source

protected theorem injective : Function.Injective e :=
  e.toEquiv.injective

Injectivity of Linear Equivalences

Informal description

For any linear equivalence (semilinear isomorphism) $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$, the underlying map $e : M \to M_2$ is injective. That is, for any $x, y \in M$, if $e(x) = e(y)$, then $x = y$.

LinearEquiv.surjective theorem

: Function.Surjective e

Full source

protected theorem surjective : Function.Surjective e :=
  e.toEquiv.surjective

Surjectivity of Semilinear Equivalences

Informal description

For any semilinear equivalence $e : M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, the underlying map $e : M \to M_2$ is surjective.

LinearEquiv.image_eq_preimage theorem

(s : Set M) : e '' s = e.symm ⁻¹' s

Full source

protected theorem image_eq_preimage (s : Set M) : e '' s = e.symm ⁻¹' s :=
  e.toEquiv.image_eq_preimage s

Image-Preimage Correspondence for Semilinear Equivalences

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, and for any subset $s \subseteq M$, the image of $s$ under $e$ equals the preimage of $s$ under the inverse equivalence $e^{-1}$, i.e., \[ e(s) = e^{-1}^{-1}(s). \]

LinearEquiv.image_symm_eq_preimage theorem

(s : Set M₂) : e.symm '' s = e ⁻¹' s

Full source

protected theorem image_symm_eq_preimage (s : Set M₂) : e.symm '' s = e ⁻¹' s :=
  e.toEquiv.symm.image_eq_preimage s

Image-Preimage Correspondence for Inverse Semilinear Equivalence

Informal description

For any semilinear equivalence $e \colon M \simeq_{\sigma} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $S$ respectively, and for any subset $s \subseteq M_2$, the image of $s$ under the inverse equivalence $e^{-1}$ is equal to the preimage of $s$ under $e$, i.e., \[ e^{-1}(s) = e^{-1}(s). \]

RingEquiv.toSemilinearEquiv definition

 (f : R ≃+* S) :
  haveI := RingHomInvPair.of_ringEquiv f
  haveI := RingHomInvPair.symm (↑f : R →+* S) (f.symm : S →+* R)
  R ≃ₛₗ[(↑f : R →+* S)] S

Full source

/-- Interpret a `RingEquiv` `f` as an `f`-semilinear equiv. -/
@[simps]
def _root_.RingEquiv.toSemilinearEquiv (f : R ≃+* S) :
    haveI := RingHomInvPair.of_ringEquiv f
    haveI := RingHomInvPair.symm (↑f : R →+* S) (f.symm : S →+* R)
    R ≃ₛₗ[(↑f : R →+* S)] S :=
  haveI := RingHomInvPair.of_ringEquiv f
  haveI := RingHomInvPair.symm (↑f : R →+* S) (f.symm : S →+* R)
  { f with
    toFun := f
    map_smul' := f.map_mul }

Semilinear equivalence induced by a ring isomorphism

Informal description

Given a ring isomorphism $f: R \simeq S$, the function constructs a semilinear equivalence between $R$ and $S$ viewed as modules over themselves, where the scalar multiplication is twisted by $f$. Specifically, the equivalence maps $x \in R$ to $f(x) \in S$ and satisfies $f(r \cdot x) = f(r) \cdot f(x)$ for all $r, x \in R$.

LinearEquiv.ofInvolutive definition

 {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {_ : Module R M} (f : M →ₛₗ[σ] M) (hf : Involutive f) :
  M ≃ₛₗ[σ] M

Full source

/-- An involutive linear map is a linear equivalence. -/
def ofInvolutive {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    {_ : Module R M} (f : M →ₛₗ[σ] M) (hf : Involutive f) : M ≃ₛₗ[σ] M :=
  { f, hf.toPerm f with }

Linear equivalence from an involutive semilinear map

Informal description

Given a semiring $R$, a module $M$ over $R$, and a semilinear map $f: M \to M$ with respect to a ring homomorphism $\sigma: R \to R$ (where $\sigma$ and its inverse $\sigma'$ satisfy compatibility conditions), if $f$ is involutive (i.e., $f(f(x)) = x$ for all $x \in M$), then $f$ defines a linear equivalence between $M$ and itself. This means $f$ is an invertible semilinear map where the inverse is also $f$, and it preserves the module structure up to the action of $\sigma$.

LinearEquiv.coe_ofInvolutive theorem

 {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {_ : Module R M} (f : M →ₛₗ[σ] M) (hf : Involutive f) :
  ⇑(ofInvolutive f hf) = f

Full source

@[simp]
theorem coe_ofInvolutive {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    {_ : Module R M} (f : M →ₛₗ[σ] M) (hf : Involutive f) : ⇑(ofInvolutive f hf) = f :=
  rfl

Coercion of Involutive Semilinear Equivalence Equals Original Map

Informal description

Let $R$ be a semiring and $M$ be a module over $R$. Given a semilinear map $f: M \to M$ with respect to a ring homomorphism $\sigma: R \to R$ (where $\sigma$ and its inverse $\sigma'$ satisfy the compatibility conditions `RingHomInvPair σ σ'` and `RingHomInvPair σ' σ`), if $f$ is involutive (i.e., $f(f(x)) = x$ for all $x \in M$), then the underlying function of the linear equivalence $\text{ofInvolutive}\, f\, hf$ is equal to $f$. In other words, the coercion of the linear equivalence constructed from an involutive semilinear map $f$ is $f$ itself.

Mathlib.Algebra.Module.Equiv.Defs

Implementation notes

TODO

Tags