Module

FiniteFamilyLinearMap.lean

Nyll.ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap

9 declarations indexed from sourceView source ↗

Module documentation

Fox differential: common — finite family linear map

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.

Imports1

Mathlib.Algebra.Exact.Basic

Imported by3

def

finiteFamilyLinearMap

L38 ↗

FoxDifferential.finiteFamilyLinearMap

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]

Lean source · full declaration

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]

theorem

finiteFamilyLinearMap_apply

L51 ↗

FoxDifferential.finiteFamilyLinearMap_apply

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem finiteFamilyLinearMap_apply (generators : X → M) (x : X → R) :
    finiteFamilyLinearMap (R := R) generators x = ∑ i, x i • generators i

theorem

finiteFamilyLinearMap_single

L56 ↗

FoxDifferential.finiteFamilyLinearMap_single

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]

Lean source · statement

theorem finiteFamilyLinearMap_single (generators : X → M) (i : X) :
    finiteFamilyLinearMap (R := R) generators (Pi.single i 1) = generators i

def

piReindexLinearEquiv

L70 ↗

FoxDifferential.piReindexLinearEquiv

Documentation

Reindex finite coordinate functions by an equivalence of index types.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
section Reindex
variable {Y : Type*} [Fintype Y] [DecidableEq Y]

Lean source · full declaration

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]

theorem

finiteFamilyLinearMap_reindex

L93 ↗

FoxDifferential.finiteFamilyLinearMap_reindex

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
section Reindex
variable {Y : Type*} [Fintype Y] [DecidableEq Y]
omit [DecidableEq X] [DecidableEq Y] in

Lean source · full declaration

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 := by
  apply LinearMap.ext
  intro f
  rw [finiteFamilyLinearMap_apply, LinearMap.comp_apply, finiteFamilyLinearMap_apply]
  exact
    Fintype.sum_equiv e
      (fun x : X => f x • generators (e x))
      (fun y : Y => f (e.symm y) • generators y)
      (by intro x; simp only [Equiv.symm_apply_apply])

theorem

finiteFamilyLinearMap_leftInverse_of_mapsToSingle

L113 ↗

FoxDifferential.finiteFamilyLinearMap_leftInverse_of_mapsToSingle

Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]

Lean source · statement

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

theorem

finiteFamilyLinearMap_range_eq_span

L147 ↗

FoxDifferential.finiteFamilyLinearMap_range_eq_span

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem finiteFamilyLinearMap_range_eq_span (generators : X → M) :
    LinearMap.range (finiteFamilyLinearMap (R := R) generators) =
      Submodule.span R (Set.range generators)

theorem

finiteFamilyLinearMap_surjective_of_span_eq_top

L164 ↗

FoxDifferential.finiteFamilyLinearMap_surjective_of_span_eq_top

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem finiteFamilyLinearMap_surjective_of_span_eq_top
    (generators : X → M)
    (hspan : Submodule.span R (Set.range generators) = ⊤) :
    Function.Surjective (finiteFamilyLinearMap (R := R) generators)

theorem

finiteFamilyLinearMap_surjective_iff_span_eq_top

L173 ↗

FoxDifferential.finiteFamilyLinearMap_surjective_iff_span_eq_top

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
section FiniteFamilyLinearMap
variable {R : Type*} [Semiring R]
variable {M : Type*} [AddCommMonoid M] [Module R M]
variable {X : Type*} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem finiteFamilyLinearMap_surjective_iff_span_eq_top
    {generators : X → M} :
    Function.Surjective (finiteFamilyLinearMap (R := R) generators) ↔
      Submodule.span R (Set.range generators) = ⊤

Module documentation

Fox differential: common — finite family linear map

Declarations