4.6. Base change and field towers🔗

Lemma4.6.1

uses 1used by 0✓L∃∀N

Tagslean-only

Rank and stress dimension are unchanged by extending the coefficient field along L \subseteq K, and by restricting a placement to a subtype of vertices after a deletion.

Lean code for Lemma4.6.1●3 theorems

theoremdefined in RB31EndToEnd/Linear/FiniteFamilyBaseChange.lean

complete

theorem RB31E2E.FiniteFamilyBaseChange.finrank_span_range_mapVector.{u_1, u_2,
    u_3, u_4}
  {L : Type u_1} {K : Type u_2} {I : Type u_3} {J : Type u_4} [Field L]
  [Field K] [Algebra L K] [Finite J] (v : I → J → L) :
  Module.finrank L ↥(Submodule.span L (Set.range v)) =
    Module.finrank K
      ↥(Submodule.span K
          (Set.range fun i ↦
            RB31E2E.FiniteFamilyBaseChange.mapVector (v i)))

theorem RB31E2E.FiniteFamilyBaseChange.finrank_span_range_mapVector.{u_1,
    u_2, u_3, u_4}
  {L : Type u_1} {K : Type u_2}
  {I : Type u_3} {J : Type u_4} [Field L]
  [Field K] [Algebra L K] [Finite J]
  (v : I → J → L) :
  Module.finrank L
      ↥(Submodule.span L (Set.range v)) =
    Module.finrank K
      ↥(Submodule.span K
          (Set.range fun i ↦
            RB31E2E.FiniteFamilyBaseChange.mapVector
              (v i)))

The span rank of a finite vector family is invariant under a field
extension.

theoremdefined in RB31EndToEnd/Linear/DirectionStressBaseChange.lean

complete

theorem RB31E2E.DirectionStress.directionStressDim_mapPlacement.{u_1, u_2, u_3}
  {L : Type u_1} {K : Type u_2} {V : Type u_3} [Field L] [Field K]
  [Algebra L K] [Fintype V] [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → L) :
  RB31E2E.DirectionStress.directionStressDim F
      (RB31E2E.DirectionStress.mapPlacement a) =
    RB31E2E.DirectionStress.directionStressDim F a

theorem RB31E2E.DirectionStress.directionStressDim_mapPlacement.{u_1,
    u_2, u_3}
  {L : Type u_1} {K : Type u_2}
  {V : Type u_3} [Field L] [Field K]
  [Algebra L K] [Fintype V]
  [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V)
  (a : V → Fin 3 → L) :
  RB31E2E.DirectionStress.directionStressDim
      F
      (RB31E2E.DirectionStress.mapPlacement
        a) =
    RB31E2E.DirectionStress.directionStressDim
      F a

Direction-stress nullity is invariant under a field extension.

theoremdefined in RB31EndToEnd/Linear/DirectionStressVertexDeletion.lean

complete

theorem RB31E2E.DirectionStress.directionStressDim_restrictedLiveEdges.{u_1,
    u_2}
  {k : Type u_1} {V : Type u_2} [Field k] [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) (v : V) :
  RB31E2E.DirectionStress.directionStressDim
      (RB31E2E.ProvenanceFlag.restrictedLiveEdges F v)
      (RB31E2E.DirectionStress.restrictPlacement a v) =
    RB31E2E.DirectionStress.directionStressDim
      (RB31E2E.deleteVertexEdges F v) a

theorem RB31E2E.DirectionStress.directionStressDim_restrictedLiveEdges.{u_1,
    u_2}
  {k : Type u_1} {V : Type u_2} [Field k]
  [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V)
  (a : V → Fin 3 → k) (v : V) :
  RB31E2E.DirectionStress.directionStressDim
      (RB31E2E.ProvenanceFlag.restrictedLiveEdges
        F v)
      (RB31E2E.DirectionStress.restrictPlacement
        a v) =
    RB31E2E.DirectionStress.directionStressDim
      (RB31E2E.deleteVertexEdges F v) a

Stress nullity is exactly invariant under the literal child reindexing.

The paper moves between coefficient fields without comment: "the rank of a finite matrix is unchanged by a field extension" is one clause of (2.5), A_K = D_H(a_H)^T \otimes_L K is one clause of (2.1), and the descent lemma identifies R \otimes_L K with the image of a scalar extension in one line of its proof. Each of those clauses is a theorem in the formalization, and the deletion step uses all of them; the supporting development spans coordinate field towers, finite row systems and localization arithmetic.

The vertex type changes as well as the field. In the paper, H = F - v is a graph on a subset of the same ambient vertex set, so nothing has to be transported. In the formalization, deleting v from a graph on V leaves a graph on the subtype \{u : u \ne v\}, so a stress space has to be moved along the inclusion and the two presentations proved to have the same dimension — the same convention that makes the sparsity transport lemma necessary.