Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap
ProCGroups/FoxDifferential/Common/FiniteFamilyLinearMap

ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap

7 Theorems | 2 Definitions

The principal declarations in this module are:

  • finiteFamilyLinearMap The linear map represented by a finite family of target vectors. - piReindexLinearEquiv Reindex finite coordinate functions by an equivalence of index types. - finiteFamilyLinearMap_apply The linear map represented by generators evaluates a coordinate vector as the finite sum ∑ i, x i • generators i. - finiteFamilyLinearMap_single A finite-family linear map sends a coordinate basis vector to the corresponding generator.
import
  • Mathlib.Algebra.Exact.Basic
Imported by

Declarations

Definition FoxDifferential.finiteFamilyLinearMap 
def finiteFamilyLinearMap (generators : X → M) :
    (X → R) →ₗ[R] M where
  toFun x := ∑ i, x i • generators i
  map_add' x y := by
    simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
  map_smul' a x := by
    simp only [Pi.smul_apply, smul_eq_mul, mul_smul, RingHom.id_apply, Finset.smul_sum]

The linear map represented by a finite family of target vectors.

Theorem FoxDifferential.finiteFamilyLinearMap_apply 
omit [DecidableEq X] in
theorem finiteFamilyLinearMap_apply (generators : X → M) (x : X → R) :
    finiteFamilyLinearMap (R := R) generators x = ∑ i, x i • generators i

The linear map represented by generators evaluates a coordinate vector as the finite sum ∑ i, x i • generators i.

Show Lean proof
Theorem FoxDifferential.finiteFamilyLinearMap_single 
@[simp 900]
theorem finiteFamilyLinearMap_single (generators : X → M) (i : X) :
    finiteFamilyLinearMap (R := R) generators (Pi.single i 1) = generators i

A finite-family linear map sends a coordinate basis vector to the corresponding generator.

Show Lean proof
Definition FoxDifferential.piReindexLinearEquiv 
def piReindexLinearEquiv (e : X ≃ Y) :
    (X → R) ≃ₗ[R] (Y → R) where
  toFun f := fun y => f (e.symm y)
  invFun f := fun x => f (e x)
  left_inv := by
    intro f
    funext x
    simp only [Equiv.symm_apply_apply]
  right_inv := by
    intro f
    funext y
    simp only [Equiv.apply_symm_apply]
  map_add' := by
    intro f g
    funext y
    simp only [Pi.add_apply]
  map_smul' := by
    intro a f
    funext y
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]

Reindex finite coordinate functions by an equivalence of index types.

Theorem FoxDifferential.finiteFamilyLinearMap_reindex 
omit [DecidableEq X] [DecidableEq Y] in
theorem finiteFamilyLinearMap_reindex
    (e : X ≃ Y) (generators : Y → M) :
    finiteFamilyLinearMap (R := R) (fun x : X => generators (e x)) =
      (finiteFamilyLinearMap (R := R) generators).comp
        (piReindexLinearEquiv (R := R) e).toLinearMap

Finite-family linear maps are invariant under reindexing of their finite coordinate type.

Show Lean proof
Theorem FoxDifferential.finiteFamilyLinearMap_leftInverse_of_mapsToSingle 
theorem finiteFamilyLinearMap_leftInverse_of_mapsToSingle
    (generators : X → M) (coordinateMap : M →ₗ[R] (X → R))
    (hcoord : ∀ i : X, coordinateMap (generators i) = Pi.single i 1) :
    coordinateMap.comp (finiteFamilyLinearMap (R := R) generators) = LinearMap.id

A coordinate map sending a finite generating family to the standard basis is a left inverse to the corresponding finite-family linear map.

Show Lean proof
Theorem FoxDifferential.finiteFamilyLinearMap_range_eq_span 
omit [DecidableEq X] in
theorem finiteFamilyLinearMap_range_eq_span (generators : X → M) :
    LinearMap.range (finiteFamilyLinearMap (R := R) generators) =
      Submodule.span R (Set.range generators)

The image of a finite-family linear map is exactly the submodule spanned by its target family.

Show Lean proof
Theorem FoxDifferential.finiteFamilyLinearMap_surjective_of_span_eq_top 
omit [DecidableEq X] in
theorem finiteFamilyLinearMap_surjective_of_span_eq_top
    (generators : X → M)
    (hspan : Submodule.span R (Set.range generators) = ⊤) :
    Function.Surjective (finiteFamilyLinearMap (R := R) generators)

A finite-family linear map is surjective when its target family spans the codomain.

Show Lean proof
Theorem FoxDifferential.finiteFamilyLinearMap_surjective_iff_span_eq_top 
omit [DecidableEq X] in
theorem finiteFamilyLinearMap_surjective_iff_span_eq_top
    {generators : X → M} :
    Function.Surjective (finiteFamilyLinearMap (R := R) generators) ↔
      Submodule.span R (Set.range generators) = ⊤

Surjectivity of a finite-family map is exactly the statement that the target family spans.

Show Lean proof