Module

FreeCrossedDifferential.lean

Nyll.ProCGroups.FoxDifferential.Common.FreeCrossedDifferential

50 declarations indexed from sourceView source ↗

Module documentation

Fox differential: common — free crossed differential

The principal declarations in this module are:

freeCrossedHomActionLift

The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive action.

freeCrossedHomForAction

The free crossed homomorphism with prescribed generator values for a general additive action. This is the canonical action-level construction; scalar Fox differentials specialize it via scalarCrossedAction.

freeCrossedHomActionLift_right

The free-group component of semidirect multiplication.

freeCrossedHomForAction_of

The free crossed homomorphism takes each free generator to its prescribed basis value.

Imports3

Nyll.ProCGroups.FoxDifferential.Common.CrossedDifferential
Nyll.ProCGroups.FoxDifferential.Common.Jacobian
Mathlib.GroupTheory.FreeGroup.Basic

Imported by5

def

freeCrossedHomActionLift

L47 ↗

FoxDifferential.freeCrossedHomActionLift

Documentation

The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary additive action.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · statement

def freeCrossedHomActionLift :
    FreeGroup X →* CrossedSemidirectProduct action

theorem

freeCrossedHomActionLift_right

L53 ↗

FoxDifferential.freeCrossedHomActionLift_right

Documentation

The free-group component of semidirect multiplication.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomActionLift_right (w : FreeGroup X) :
    (freeCrossedHomActionLift action basisValue w).right = w

def

freeCrossedHomForAction

L65 ↗

FoxDifferential.freeCrossedHomForAction

Documentation

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · statement

def freeCrossedHomForAction : CrossedHom action

theorem

freeCrossedHomForAction_of

L72 ↗

FoxDifferential.freeCrossedHomForAction_of

Documentation

The free crossed homomorphism takes each free generator to its prescribed basis value.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomForAction_of (x : X) :
    freeCrossedHomForAction action basisValue (FreeGroup.of x) = basisValue x

theorem

freeCrossedHomForAction_unique

L81 ↗

FoxDifferential.freeCrossedHomForAction_unique

Documentation

A crossed homomorphism on a free group is determined by its values on the free generators, for an arbitrary additive action.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomForAction_unique
    (delta : CrossedHom action)
    (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
    delta = freeCrossedHomForAction action basisValue

def

crossedHomForActionEquivGeneratorValues

L95 ↗

FoxDifferential.crossedHomForActionEquivGeneratorValues

Documentation

General-action crossed homomorphisms on a free group are equivalent to generator-value assignments.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
section GeneralAction
variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)

Lean source · full declaration

def crossedHomForActionEquivGeneratorValues : CrossedHom action ≃ (X → A) where
  toFun delta x := delta (FreeGroup.of x)
  invFun values := freeCrossedHomForAction action values
  left_inv delta := (freeCrossedHomForAction_unique action
    (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
  right_inv values := by
    funext x
    exact freeCrossedHomForAction_of action values x

def

freeCrossedDifferentialWithCoeffLift

L112 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffLift

Documentation

The semidirect lift whose left component is the free crossed differential with prescribed generator values.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

def freeCrossedDifferentialWithCoeffLift :
    FreeGroup X →* CrossedSemidirectProduct (scalarCrossedAction (A := A) coeff)

def

freeCrossedDifferentialWithCoeff

L118 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff

Documentation

The free crossed differential with coefficient homomorphism coeff and prescribed generator values basisValue.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

def freeCrossedDifferentialWithCoeff (w : FreeGroup X) : A

theorem

freeCrossedDifferentialWithCoeffLift_right

L124 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffLift_right

Documentation

The right component of the free crossed-differential lift is the identity on the free group.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedDifferentialWithCoeffLift_right (w : FreeGroup X) :
    (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).right = w

theorem

freeCrossedDifferentialWithCoeff_one

L131 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff_one

Documentation

The free crossed differential sends the identity word to zero.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedDifferentialWithCoeff_one :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue 1 = 0

theorem

freeCrossedDifferentialWithCoeff_of

L140 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff_of

Documentation

The free crossed differential sends a free generator to its prescribed value.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedDifferentialWithCoeff_of (x : X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (FreeGroup.of x) =
      basisValue x

theorem

freeCrossedDifferentialWithCoeff_mul

L151 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff_mul

Documentation

Product rule for the free crossed differential with arbitrary coefficients.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedDifferentialWithCoeff_mul (u v : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (u * v) =
      freeCrossedDifferentialWithCoeff (A := A) coeff basisValue u +
        coeff u • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue v

theorem

freeCrossedDifferentialWithCoeff_inv

L164 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff_inv

Documentation

Inverse rule for the free crossed differential with arbitrary coefficients.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedDifferentialWithCoeff_inv (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w⁻¹ =
      -(coeff w⁻¹ • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w)

def

freeCrossedHomWithCoeff

L178 ↗

FoxDifferential.freeCrossedHomWithCoeff

Documentation

The free crossed differential with coefficient homomorphism \(\mathrm{coeff}\) and prescribed generator values \(\mathrm{basisValue}\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

def freeCrossedHomWithCoeff : ScalarCrossedHom coeff A

theorem

freeCrossedHomWithCoeff_apply

L184 ↗

FoxDifferential.freeCrossedHomWithCoeff_apply

Documentation

Evaluating the bundled free crossed homomorphism gives the corresponding free crossed differential.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomWithCoeff_apply (w : FreeGroup X) :
    freeCrossedHomWithCoeff (A := A) coeff basisValue w =
      freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w

theorem

freeCrossedHomWithCoeff_of

L191 ↗

FoxDifferential.freeCrossedHomWithCoeff_of

Documentation

The free crossed differential sends a free generator to its prescribed value.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomWithCoeff_of (x : X) :
    freeCrossedHomWithCoeff (A := A) coeff basisValue (FreeGroup.of x) = basisValue x

theorem

freeCrossedHomWithCoeff_unique

L199 ↗

FoxDifferential.freeCrossedHomWithCoeff_unique

Documentation

Uniqueness of crossed differentials on a free group from their generator values, for an arbitrary coefficient homomorphism.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem freeCrossedHomWithCoeff_unique
    (delta : ScalarCrossedHom coeff A)
    (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
    delta = freeCrossedHomWithCoeff (A := A) coeff basisValue

theorem

existsUnique_freeCrossedHomWithCoeff

L210 ↗

FoxDifferential.existsUnique_freeCrossedHomWithCoeff

Documentation

Existence and uniqueness of crossed differentials on a free group from arbitrary generator values and an arbitrary coefficient homomorphism.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · statement

theorem existsUnique_freeCrossedHomWithCoeff :
    ∃! delta : ScalarCrossedHom coeff A,
      ∀ x : X, delta (FreeGroup.of x) = basisValue x

def

crossedHomEquivGeneratorValues

L222 ↗

FoxDifferential.crossedHomEquivGeneratorValues

Documentation

Crossed differentials on a free group are equivalent to assignments of values on the free generators.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)

Lean source · full declaration

def crossedHomEquivGeneratorValues : ScalarCrossedHom coeff A ≃ (X → A) where
  toFun delta := fun x => delta (FreeGroup.of x)
  invFun basisValue := freeCrossedHomWithCoeff (A := A) coeff basisValue
  left_inv delta := by
    exact (freeCrossedHomWithCoeff_unique (A := A) coeff
      (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
  right_inv basisValue := by
    funext x
    exact freeCrossedHomWithCoeff_of (A := A) coeff basisValue x

def

freeCrossedDifferentialWithCoeffCoordinates

L241 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates

Documentation

The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism to a ring.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

def freeCrossedDifferentialWithCoeffCoordinates
    (coeff : FreeGroup X →* S) (w : FreeGroup X) : X → S

def

freeCrossedHomWithCoeffCoordinates

L250 ↗

FoxDifferential.freeCrossedHomWithCoeffCoordinates

Documentation

The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism to a ring.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

def freeCrossedHomWithCoeffCoordinates
    (coeff : FreeGroup X →* S) : ScalarCrossedHom coeff (X → S)

theorem

freeCrossedHomWithCoeffCoordinates_apply

L258 ↗

FoxDifferential.freeCrossedHomWithCoeffCoordinates_apply

Documentation

Evaluating the bundled coordinate crossed homomorphism gives the unbundled coordinate differential.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedHomWithCoeffCoordinates_apply
    (coeff : FreeGroup X →* S) (w : FreeGroup X) :
    freeCrossedHomWithCoeffCoordinates (X := X) coeff w =
      freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff w

theorem

freeCrossedDifferentialWithCoeffCoordinates_one

L266 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_one

Documentation

The coordinate crossed differential sends the identity word to zero.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffCoordinates_one
    (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (1 : FreeGroup X) = 0

theorem

freeCrossedDifferentialWithCoeffCoordinates_of

L273 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_of

Documentation

The coordinate crossed differential sends a generator to the standard coordinate vector.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffCoordinates_of
    (coeff : FreeGroup X →* S) (x : X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (FreeGroup.of x) =
      Pi.single x (1 : S)

def

freeCrossedDifferentialWithCoeffExpansionLinearMap

L280 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap

Documentation

The finite linear map evaluating a coordinate vector on prescribed generator values.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · full declaration

def freeCrossedDifferentialWithCoeffExpansionLinearMap
    [Fintype X] (basisValue : X → B) : (X → S) →ₗ[S] B where
  toFun v := ∑ x : X, v x • basisValue x
  map_add' v w := by
    simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
  map_smul' a v := by
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]

theorem

freeCrossedDifferentialWithCoeffExpansionLinearMap_apply

L291 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap_apply

Documentation

The coefficient-expansion linear map evaluates v as ∑ x, v x • basisValue x.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_apply
    [Fintype X] (basisValue : X → B) (v : X → S) :
    freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue v =
      ∑ x : X, v x • basisValue x

theorem

freeCrossedDifferentialWithCoeffExpansionLinearMap_single

L299 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffExpansionLinearMap_single

Documentation

The expansion linear map sends a standard coordinate vector to the corresponding value.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_single
    [Fintype X] (basisValue : X → B) (x : X) :
    freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue
        (Pi.single x (1 : S)) =
      basisValue x

def

freeCrossedDifferentialWithCoeffExpansion

L312 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffExpansion

Documentation

The Fox-coordinate expansion determined by arbitrary coefficient coordinates.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

def freeCrossedDifferentialWithCoeffExpansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B)
    (w : FreeGroup X) : B

def

freeCrossedHomWithCoeffExpansion

L319 ↗

FoxDifferential.freeCrossedHomWithCoeffExpansion

Documentation

Arbitrary coefficient coordinates determine the Fox-coordinate expansion.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

def freeCrossedHomWithCoeffExpansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) :
    ScalarCrossedHom coeff B

theorem

freeCrossedHomWithCoeffExpansion_apply

L329 ↗

FoxDifferential.freeCrossedHomWithCoeffExpansion_apply

Documentation

Evaluating the bundled coordinate expansion gives the corresponding unbundled Fox expansion.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedHomWithCoeffExpansion_apply
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
    freeCrossedHomWithCoeffExpansion (X := X) coeff basisValue w =
      freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w

theorem

freeCrossedDifferentialWithCoeffExpansion_of

L337 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffExpansion_of

Documentation

The coefficient-coordinate expansion sends each generator to its prescribed value.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffExpansion_of
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (x : X) :
    freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue (FreeGroup.of x) =
      basisValue x

theorem

freeCrossedDifferentialWithCoeff_eq_expansion

L346 ↗

FoxDifferential.freeCrossedDifferentialWithCoeff_eq_expansion

Documentation

A free crossed differential is its coefficient-coordinate expansion.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeff_eq_expansion
    [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeff (A := B) coeff basisValue w =
      freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w

theorem

freeCrossedHomWithCoeff_comp_expansion

L360 ↗

FoxDifferential.freeCrossedHomWithCoeff_comp_expansion

Documentation

Abstract Fox chain rule: composing a crossed differential with a free-group homomorphism is the coordinate expansion using the pulled-back coefficient homomorphism.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · full declaration

theorem freeCrossedHomWithCoeff_comp_expansion
    [Fintype X]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (delta : ScalarCrossedHom coeff B) (w : FreeGroup X) :
    delta (φ w) =
      freeCrossedDifferentialWithCoeffExpansion
        (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
  let pulled : ScalarCrossedHom (coeff.comp φ) B :=
    ScalarCrossedHom.compMonoidHom delta φ
  have hunique :
      pulled =
        freeCrossedHomWithCoeff
          (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) :=
    freeCrossedHomWithCoeff_unique
      (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x)))
      pulled (by intro x; rfl)
  calc
    delta (φ w) = pulled w := rfl
    _ =
        freeCrossedDifferentialWithCoeff
          (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
          exact congrArg (fun d : ScalarCrossedHom (coeff.comp φ) B => d w) hunique
    _ =
        freeCrossedDifferentialWithCoeffExpansion
          (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
          exact freeCrossedDifferentialWithCoeff_eq_expansion
            (X := X) (B := B) (coeff.comp φ)
            (fun x : X => delta (φ (FreeGroup.of x))) w

def

freeCrossedDifferentialWithCoeffJacobian

L391 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobian

Documentation

The abstract Fox-Jacobian of a homomorphism of free sources, with coefficients in S.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

def freeCrossedDifferentialWithCoeffJacobian
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    X → Y → S

def

freeCrossedDifferentialWithCoeffJacobianMatrix

L398 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix

Documentation

The abstract Fox-Jacobian of a free-source homomorphism as a matrix.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

def freeCrossedDifferentialWithCoeffJacobianMatrix
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    Matrix X Y S

theorem

freeCrossedDifferentialWithCoeffJacobianMatrix_apply

L406 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_apply

Documentation

The abstract Fox-Jacobian matrix entry is the corresponding Fox-Jacobian component.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianMatrix_apply
    [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (x : X) (y : Y) :
    freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ x y =
      freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

def

freeCrossedDifferentialWithCoeffJacobianLinearMap

L418 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap

Documentation

The abstract Fox-Jacobian determines a finite linear map between the corresponding free coefficient modules.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

def freeCrossedDifferentialWithCoeffJacobianLinearMap
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
    (X → S) →ₗ[S] (Y → S)

theorem

freeCrossedDifferentialWithCoeffJacobianLinearMap_apply

L430 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_apply

Documentation

Evaluation of the linear map associated with the abstract Fox-Jacobian is computed by the corresponding matrix coefficient formula.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_apply
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (v : X → S) (y : Y) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v y =
      ∑ x : X, v x * freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

theorem

freeCrossedDifferentialWithCoeffJacobianLinearMap_single

L440 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_single

Documentation

The abstract Fox-Jacobian linear map sends a source basis vector to the corresponding row.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_single
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (x : X) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
        (Pi.single x (1 : S)) =
      freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x

theorem

freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul

L451 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul

Documentation

The abstract Fox-Jacobian linear map is row-vector multiplication by its matrix.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (v : X → S) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v =
      Matrix.vecMul v
        (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ)

theorem

freeCrossedDifferentialWithCoeffJacobian_id

L462 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_id

Documentation

The abstract Fox-Jacobian of the identity homomorphism is the identity family.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobian_id (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobian
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      foxJacobianId (R := S) (X := X)

theorem

freeCrossedDifferentialWithCoeffJacobianMatrix_id

L472 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_id

Documentation

The abstract Fox-Jacobian matrix of the identity homomorphism is the identity matrix.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianMatrix_id (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobianMatrix
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      (1 : Matrix X X S)

theorem

freeCrossedDifferentialWithCoeffJacobianLinearMap_id

L482 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_id

Documentation

The abstract Fox-Jacobian linear map of the identity homomorphism is the identity.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_id
    [Fintype X] (coeff : FreeGroup X →* S) :
    freeCrossedDifferentialWithCoeffJacobianLinearMap
        (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
      (LinearMap.id : (X → S) →ₗ[S] (X → S))

theorem

freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap

L492 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap

Documentation

Abstract Fox chain rule for coordinate vectors, written as a Jacobian linear-map identity.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
      freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
        (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)

theorem

freeCrossedDifferentialWithCoeffCoordinates_comp_apply

L524 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_apply

Documentation

Component form of the abstract Fox chain rule: the pushed-forward coordinate is the sum over source coordinates weighted by the Fox-Jacobian.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_apply
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) (y : Y) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) y =
      ∑ x : X,
        freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w x *
          freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y

theorem

freeCrossedDifferentialWithCoeffCoordinates_comp_matrix

L537 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffCoordinates_comp_matrix

Documentation

Abstract Fox chain rule for coordinate vectors, written as matrix multiplication.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]

Lean source · statement

theorem freeCrossedDifferentialWithCoeffCoordinates_comp_matrix
    [Fintype X] [DecidableEq Y]
    (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
    (w : FreeGroup X) :
    freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
      Matrix.vecMul
        (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)
        (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ)

theorem

freeCrossedDifferentialWithCoeffJacobian_comp_apply

L555 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_comp_apply

Documentation

Component form of the abstract Fox-Jacobian chain rule for a composite of free-group homomorphisms.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobian_comp_apply
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
    (x : X) (z : Z) :
    freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) x z =
      ∑ y : Y,
        freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
          freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z

theorem

freeCrossedDifferentialWithCoeffJacobian_comp

L570 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobian_comp

Documentation

The abstract Fox-Jacobian chain rule is expressed in family form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · full declaration

theorem freeCrossedDifferentialWithCoeffJacobian_comp
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) =
      fun x z =>
        ∑ y : Y,
          freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
            freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z := by
  funext x z
  exact freeCrossedDifferentialWithCoeffJacobian_comp_apply
    (X := X) (Y := Y) coeff φ χ x z

theorem

freeCrossedDifferentialWithCoeffJacobianLinearMap_comp

L585 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianLinearMap_comp

Documentation

The abstract Fox-Jacobian chain rule is expressed in linear-map form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_comp
    {Z : Type*} [Fintype X] [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    (freeCrossedDifferentialWithCoeffJacobianLinearMap (X := Y) (Y := Z) coeff φ).comp
        (freeCrossedDifferentialWithCoeffJacobianLinearMap
          (X := X) (Y := Y) (coeff.comp φ) χ) =
      freeCrossedDifferentialWithCoeffJacobianLinearMap
        (X := X) (Y := Z) coeff (φ.comp χ)

theorem

freeCrossedDifferentialWithCoeffJacobianMatrix_comp

L609 ↗

FoxDifferential.freeCrossedDifferentialWithCoeffJacobianMatrix_comp

Documentation

The abstract Fox-Jacobian chain rule is expressed in matrix form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {R : Type*} [Semiring R]
variable {A : Type*} [AddCommGroup A] [Module R A]
variable {X : Type u}
variable (coeff : FreeGroup X →* R) (basisValue : X → A)
section Coordinates
variable {S : Type*} [Ring S]
variable {B : Type*} [AddCommGroup B] [Module S B]
variable {Y : Type v}
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeCrossedDifferentialWithCoeffJacobianMatrix_comp
    {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
    (coeff : FreeGroup Z →* S)
    (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
    freeCrossedDifferentialWithCoeffJacobianMatrix
        (X := X) (Y := Z) coeff (φ.comp χ) =
      freeCrossedDifferentialWithCoeffJacobianMatrix
          (X := X) (Y := Y) (coeff.comp φ) χ *
        freeCrossedDifferentialWithCoeffJacobianMatrix
          (X := Y) (Y := Z) coeff φ

Module documentation

Fox differential: common — free crossed differential

Declarations