Magnitude conjecture

MagnitudeConjecture.LinearAlgebra.DirectSumFubini

Generator formulas for direct-sum Fubini equivalences #

Small reusable lemmas for the three direct-sum operations used in orbit Fubini arguments: mapping each fiber, uncurrying a dependent pair of indices, and reindexing along an equivalence.

source
noncomputable def MagnitudeConjecture.DirectSumFubini.mapRangeLinearEquiv {R : Type uR} [Semiring R] {iota : Type uI} {beta : iota → Type uM} {gamma : iota → Type uT} [(i : iota) → AddCommMonoid (beta i)] [(i : iota) → Module R (beta i)] [(i : iota) → AddCommMonoid (gamma i)] [(i : iota) → Module R (gamma i)] (e : (i : iota) → beta i ≃ₗ[R] gamma i) :
DirectSum iota beta ≃ₗ[R] DirectSum iota gamma
Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.DirectSumFubini.mapRangeLinearEquiv_of {R : Type uR} [Semiring R] {iota : Type uI} {beta : iota → Type uM} {gamma : iota → Type uT} [DecidableEq iota] [(i : iota) → AddCommMonoid (beta i)] [(i : iota) → Module R (beta i)] [(i : iota) → AddCommMonoid (gamma i)] [(i : iota) → Module R (gamma i)] (e : (i : iota) → beta i ≃ₗ[R] gamma i) (i : iota) (x : beta i) :
    (mapRangeLinearEquiv e) ((DirectSum.of beta i) x) = (DirectSum.of gamma i) ((e i) x)
    source
    @[simp]
    theorem MagnitudeConjecture.DirectSumFubini.sigmaLcurryEquiv_symm_of_of {R : Type uR} [Semiring R] {iota : Type uI} {alpha : iota → Type uM} {T : (i : iota) → alpha i → Type uT} [DecidableEq iota] [(i : iota) → DecidableEq (alpha i)] [(i : iota) → (j : alpha i) → AddCommMonoid (T i j)] [(i : iota) → (j : alpha i) → Module R (T i j)] (i : iota) (j : alpha i) (x : T i j) :
    (DirectSum.sigmaLcurryEquiv R).symm ((DirectSum.of (fun (i : iota) => DirectSum (alpha i) (T i)) i) ((DirectSum.of (T i) j) x)) = (DirectSum.of (fun (p : (i : iota) × alpha i) => T p.fst p.snd) ⟨i, j⟩) x
    source
    @[simp]
    theorem MagnitudeConjecture.DirectSumFubini.reindexCastLinearEquiv_of {R : Type uR} [Semiring R] {iota : Type uI} {kappa : Type uM} [DecidableEq iota] [DecidableEq kappa] (e : iota ≃ kappa) {T : kappa → Type uT} [(i : kappa) → AddCommMonoid (T i)] [(i : kappa) → Module R (T i)] (i : iota) (x : T (e i)) :
    (mapRangeLinearEquiv fun (j : kappa) => LinearEquiv.cast ⋯) ((DirectSum.lequivCongrLeft R e) ((DirectSum.of (fun (i : iota) => T (e i)) i) x)) = (DirectSum.of T (e i)) x