MathlibAnnex/LinearAlgebra/Basis/Semilinear.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import Mathlib.LinearAlgebra.Basis.Defs7import Mathlib.LinearAlgebra.Finsupp.Defs89/-!10# Semilinear equivalences determined by two bases1112The scalar ring isomorphism and bases determine the map on every finitely13supported coordinate family. The basis index may be infinite. These declarations14were extracted from the projectivization construction without changing their15mathematical hypotheses or proofs; no projective incidence is needed here.16-/1718set_option autoImplicit false19noncomputable section2021namespace Module.Basis2223universe uK uL uV uW uI24variable {K : Type uK} {L : Type uL} {V : Type uV} {W : Type uW}25variable [Field K] [Field L]26variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module L W]27variable {ι : Type uI}2829local instance (σ : K ≃+* L) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=30  RingHomInvPair.of_ringEquiv σ31local instance (σ : K ≃+* L) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=32  RingHomInvPair.of_ringEquiv_symm σ3334/-- The semilinear equivalence determined by a scalar isomorphism and two35arbitrary bases. Coefficients are finitely supported; the index type need not36be finite. This construction alone does not assert agreement with a point map. -/37def semilinearEquiv (b : Module.Basis ι K V) (c : Module.Basis ι L W)38    (σ : K ≃+* L) : LinearEquiv σ.toRingHom (σ' := σ.symm.toRingHom) V W where39  toFun v := c.repr.symm (Finsupp.mapRange σ σ.map_zero (b.repr v))40  invFun w := b.repr.symm (Finsupp.mapRange σ.symm σ.symm.map_zero (c.repr w))41  left_inv v := by42    apply b.repr.injective43    ext i44    simp45  right_inv w := by46    apply c.repr.injective47    ext i48    simp49  map_add' v w := by50    apply c.repr.injective51    ext i52    simp53  map_smul' a v := by54    apply c.repr.injective55    ext i56    simp [map_mul]5758/-- Every coefficient of the actual semilinear map is prescribed. -/59@[simp]60theorem repr_semilinearEquiv (b : Module.Basis ι K V) (c : Module.Basis ι L W)61    (σ : K ≃+* L) (v : V) (i : ι) :62    c.repr (semilinearEquiv b c σ v) i = σ (b.repr v i) := by63  change c.repr (c.repr.symm (Finsupp.mapRange σ σ.map_zero (b.repr v))) i = _64  simp6566/-- The inverse has coefficient map `σ.symm`, with no choice of lifts. -/67@[simp]68theorem repr_semilinearEquiv_symm (b : Module.Basis ι K V)69    (c : Module.Basis ι L W) (σ : K ≃+* L) (w : W) (i : ι) :70    b.repr ((semilinearEquiv b c σ).symm w) i = σ.symm (c.repr w i) := by71  change b.repr (b.repr.symm (Finsupp.mapRange σ.symm σ.symm.map_zero (c.repr w))) i = _72  simp7374/-- Evaluation on each basis vector. -/75@[simp]76theorem semilinearEquiv_apply_basis (b : Module.Basis ι K V)77    (c : Module.Basis ι L W) (σ : K ≃+* L) (i : ι) :78    semilinearEquiv b c σ (b i) = c i := by79  classical80  apply c.repr.injective81  ext j82  change c.repr (semilinearEquiv b c σ (b i)) j = c.repr (c i) j83  rw [repr_semilinearEquiv]84  by_cases hij : i = j85  · subst j86    simp87  · simp [hij, Ne.symm hij]8889/-- Evaluation on every finite linear combination, not just the basis rays. -/90theorem semilinearEquiv_sum (b : Module.Basis ι K V)91    (c : Module.Basis ι L W) (σ : K ≃+* L) (s : Finset ι) (a : ι → K) :92    semilinearEquiv b c σ (∑ i ∈ s, a i • b i) =93      ∑ i ∈ s, σ (a i) • c i := by94  simp only [map_sum, map_smulₛₗ, semilinearEquiv_apply_basis]95  apply Finset.sum_congr rfl96  intro i _97  rfl9899end Module.Basis