Magnitude conjecture

MagnitudeConjecture.LinearAlgebra.FiniteDirectSumDual

Duality for a direct sum with finite nontrivial support #

The canonical map from the direct sum of the coefficient duals to the dual of a direct sum is an isomorphism when only finitely many summands are nontrivial. The construction is independent of any chosen bases.

source
noncomputable def MagnitudeConjecture.directSumLinearEquivCongrRight {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] {W : ι → Type u_1} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module k (W i)] (e : (i : ι) → V i ≃ₗ[k] W i) :
DirectSum ι V ≃ₗ[k] DirectSum ι W

A family of linear equivalences induces a linear equivalence of direct sums without changing the index.

Instances For
    source
    noncomputable def MagnitudeConjecture.directSumInclusion {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (i : ι) :
    V i →ₗ[k] DirectSum ι V

    The canonical inclusion of one summand, with the classical decidable equality choice hidden from the public interface.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.directSumInclusion_apply_self {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (i : ι) (x : V i) :
      ((directSumInclusion V i) x) i = x
      source
      theorem MagnitudeConjecture.directSumInclusion_apply_of_ne {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] {i j : ι} (hij : i ≠ j) (x : V i) :
      ((directSumInclusion V i) x) j = 0
      source
      def MagnitudeConjecture.dualComponentExtension {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (i : ι) :
      Module.Dual k (V i) →ₗ[k] Module.Dual k (DirectSum ι V)

      Extend one coefficient functional by zero on all other summands.

      Instances For
        source
        noncomputable def MagnitudeConjecture.directSumDualToDual {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] :
        (DirectSum ι fun (i : ι) => Module.Dual k (V i)) →ₗ[k] Module.Dual k (DirectSum ι V)

        Extend a finite-support family of coefficient functionals to a functional on the direct sum.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.directSumDualToDual_lof_apply {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (i : ι) (phi : Module.Dual k (V i)) (x : DirectSum ι V) :
          ((directSumDualToDual V) ((directSumInclusion (fun (j : ι) => Module.Dual k (V j)) i) phi)) x = phi (x i)
          source
          @[simp]
          theorem MagnitudeConjecture.directSumDualToDual_apply_lof {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (Phi : DirectSum ι fun (i : ι) => Module.Dual k (V i)) (i : ι) (x : V i) :
          ((directSumDualToDual V) Phi) ((directSumInclusion V i) x) = (Phi i) x
          source
          noncomputable def MagnitudeConjecture.dualToDirectSumDual {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) :
          Module.Dual k (DirectSum ι V) →ₗ[k] DirectSum ι fun (i : ι) => Module.Dual k (V i)

          Restrict a functional to each nontrivial summand and assemble the restrictions over the finite set of such summands.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.dualToDirectSumDual_apply {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) (phi : Module.Dual k (DirectSum ι V)) (i : ι) :
            ((dualToDirectSumDual V h) phi) i = (directSumInclusion V i).dualMap phi
            source
            theorem MagnitudeConjecture.directSumDualToDual_dualToDirectSumDual {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) (phi : Module.Dual k (DirectSum ι V)) :
            (directSumDualToDual V) ((dualToDirectSumDual V h) phi) = phi
            source
            theorem MagnitudeConjecture.directSumDualToDual_injective {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] :
            Function.Injective ⇑(directSumDualToDual V)
            source
            noncomputable def MagnitudeConjecture.directSumDualEquivDual {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) :
            (DirectSum ι fun (i : ι) => Module.Dual k (V i)) ≃ₗ[k] Module.Dual k (DirectSum ι V)

            The canonical, basis-free finite-duality isomorphism

            (⨁ i, Vᵢ*) ≃ (⨁ i, Vᵢ)*.

            Instances For
              source
              noncomputable def MagnitudeConjecture.directSumDualEquivDualOfFiniteDual {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (Module.Dual k (V i))}.Finite) :
              (DirectSum ι fun (i : ι) => Module.Dual k (V i)) ≃ₗ[k] Module.Dual k (DirectSum ι V)

              Variant whose finiteness hypothesis is stated on the coefficient duals. Over a field a vector space is nontrivial exactly when its dual is.

              Instances For
                source
                @[simp]
                theorem MagnitudeConjecture.directSumDualEquivDual_apply {k : Type u} [Field k] {ι : Type v} (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) (Phi : DirectSum ι fun (i : ι) => Module.Dual k (V i)) :
                (directSumDualEquivDual V h) Phi = (directSumDualToDual V) Phi