Linear equivalences and their underlying maps

Mathlib's LinearEquiv.smulOfUnit packages multiplication by a unit u of the base ring as a linear equivalence, but records no lemma evaluating it at a vector. This file supplies that evaluation lemma, in the simp-normal form that rewrites an application of LinearEquiv.smulOfUnit to a scalar multiplication. It also records how a linear automorphism, viewed as a permutation of the module through MulAction.toPermHom, moves the set underlying a submodule. For coordinate transport, forgetting linearity gives the corresponding additive word equivalence, with the same direction on coordinates.

Main results

• LinearEquiv.map_ker_of_intertwine and LinearEquiv.map_range_of_intertwine: transport of kernels and ranges across an intertwining semilinear equivalence.
• LinearEquiv.toPermHom_smul_coe: the permutation of the module underlying a linear automorphism moves the set underlying a submodule to the set underlying its image.
• LinearEquiv.smulOfUnit_apply: LinearEquiv.smulOfUnit u acts as multiplication by u.
• LinearEquiv.funCongrLeft_toAddMonoidHom: forgetting linearity in coordinate transport gives additive coordinate transport.

@[simp]

theorem LinearEquiv.funCongrLeft_toAddMonoidHom (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {κ : Type u_4} (e : κ ≃ ι) : ↑↑(funCongrLeft R M e) = ↑(AddEquiv.arrowCongr e.symm (AddEquiv.refl M))

The additive homomorphism underlying linear coordinate transport is the one underlying AddEquiv.arrowCongr, with the coordinate equivalence reversed.

theorem LinearEquiv.map_ker_of_intertwine {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) (f : M →ₗ[R] M) (g : N →ₗ[S] N) (h : ∀ (d : M), g (e d) = e (f d)) : Submodule.map (↑e) f.ker = g.ker

If a semilinear equivalence e intertwines two endomorphisms f and g pointwise (g (e d) = e (f d)), it carries the kernel of f onto the kernel of g.

theorem LinearEquiv.map_range_of_intertwine {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) (f : M →ₗ[R] M) (g : N →ₗ[S] N) (h : ∀ (d : M), g (e d) = e (f d)) : Submodule.map (↑e) f.range = g.range

If a semilinear equivalence e intertwines two endomorphisms f and g pointwise (g (e d) = e (f d)), it carries the range of f onto the range of g.

theorem LinearEquiv.toPermHom_smul_coe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (g : M ≃ₗ[R] M) (p : Submodule R M) : (MulAction.toPermHom (M ≃ₗ[R] M) M) g • ↑p = ↑(Submodule.map (↑g) p)

The permutation of the module underlying a linear automorphism moves the set underlying a submodule to the set underlying its image.

@[simp]

theorem LinearEquiv.smulOfUnit_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (u : Rˣ) (x : M) : (smulOfUnit u) x = ↑u • x

Multiplication by a unit of the base ring, evaluated: LinearEquiv.smulOfUnit u sends x to u • x.