Transporting coordinates along a ring homomorphism

Let σ : R →+* S be a ring homomorphism, b a basis of an R-module M and b' a basis of an S-module M', indexed by the same type. Applying σ to the coordinates in b and reading the result in b' gives the σ-semilinear map

Module.Basis.semilinearMap σ b b' : ∑ₖ aₖ bₖ ↦ ∑ₖ σ(aₖ) b'ₖ.

This is the comparison map between a based module and its scalar extension along σ, presented by a basis of the extension rather than by a tensor product. It applies σ to the matrices of linear maps and to determinants: a linear map g whose matrix in the bases b' is the image under σ of the matrix of a linear map f in the bases b is intertwined with f, and the determinant in b' of the image of a family is σ of its determinant in b. This is how invariants computed from matrices, such as the torsion of a based chain complex, are compared along a homomorphism of fields.

When σ is invertible, a σ-semilinear equivalence f : M ≃ₛₗ[σ] M' carries a basis b of M to the basis f ∘ b of M' (Module.Basis.mapₛₗ), and so preserves finrank (LinearEquiv.finrank_eqₛₗ). For instance, a conjugate-linear equivalence of complex vector spaces carries complex bases to complex bases.

Main declarations

• Module.Basis.semilinearMap: the σ-semilinear map sending each b k to b' k.
• Module.Basis.repr_semilinearMap_apply: its coordinates are the images of the coordinates under σ.
• Module.Basis.semilinearMap_comp_apply_of_toMatrix_eq: it intertwines two linear maps whose matrices correspond under σ.
• Module.Basis.det_comp_semilinearMap: the determinant of the image of a family is the image of its determinant.
• Module.Basis.mapₛₗ: the image of a basis under a semilinear equivalence.
• LinearEquiv.finrank_eqₛₗ: semilinear equivalences along ring isomorphisms preserve finrank.

noncomputable def Module.Basis.semilinearMap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring S] (σ : R →+* S) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (b : Basis ι R M) (b' : Basis ι S M') : M →ₛₗ[σ] M'

The σ-semilinear map ∑ₖ aₖ bₖ ↦ ∑ₖ σ(aₖ) b'ₖ, which applies the ring homomorphism σ to the coordinates in the basis b and reads the result in the basis b'.

@[simp]

theorem Module.Basis.repr_semilinearMap_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring S] (σ : R →+* S) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (b : Basis ι R M) (b' : Basis ι S M') (x : M) (k : ι) : (b'.repr ((semilinearMap σ b b') x)) k = σ ((b.repr x) k)

The coordinates of the image of a vector are the images of its coordinates.

@[simp]

theorem Module.Basis.semilinearMap_apply_self {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring S] (σ : R →+* S) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (b : Basis ι R M) (b' : Basis ι S M') (k : ι) : (semilinearMap σ b b') (b k) = b' k

The map semilinearMap σ b b' sends the basis vector b k to b' k.

theorem Module.Basis.semilinearMap_comp_apply_of_toMatrix_eq {ι : Type u_1} {κ : Type u_2} {R : Type u_3} {S : Type u_4} {M : Type u_5} {M' : Type u_6} {N : Type u_7} {N' : Type u_8} [CommSemiring R] [CommSemiring S] {σ : R →+* S} [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module S N'] [Fintype ι] [DecidableEq ι] [Finite κ] {b : Basis ι R M} {b' : Basis ι S M'} {c : Basis κ R N} {c' : Basis κ S N'} {f : M →ₗ[R] N} {g : M' →ₗ[S] N'} (h : (LinearMap.toMatrix b' c') g = ((LinearMap.toMatrix b c) f).map ⇑σ) (x : M) : g ((semilinearMap σ b b') x) = (semilinearMap σ c c') (f x)

Let f : M → N and g : M' → N' be linear maps whose matrices correspond under σ: the matrix of g in the bases b' and c' is the image under σ of the matrix of f in the bases b and c. Then g is intertwined with f by the maps semilinearMap σ b b' and semilinearMap σ c c'.

theorem Module.Basis.det_comp_semilinearMap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [CommRing R] [CommRing S] (σ : R →+* S) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module S M'] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (b' : Basis ι S M') (v : ι → M) : b'.det (⇑(semilinearMap σ b b') ∘ v) = σ (b.det v)

The determinant in the basis b' of the image of a family v is the image under σ of the determinant of v in the basis b.

noncomputable def Module.Basis.mapₛₗ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (b : Basis ι R M) (f : M ≃ₛₗ[σ] M') : Basis ι S M'

The image f ∘ b of a basis b under a σ-semilinear equivalence f, a basis over the target scalars. This is the semilinear version of Module.Basis.map.

@[simp]

theorem Module.Basis.mapₛₗ_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (b : Basis ι R M) (f : M ≃ₛₗ[σ] M') (i : ι) : (b.mapₛₗ f) i = f (b i)

theorem LinearEquiv.finrank_eqₛₗ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M' : Type u_4} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module S M'] (f : M ≃ₛₗ[σ] M') : Module.finrank R M = Module.finrank S M'

A semilinear equivalence along a ring isomorphism preserves finrank. This is the semilinear version of LinearEquiv.finrank_eq.