dualSubmodule_dualSubmodule_flip_of_basis

English

For a finite basis b of M over S, the dualSubmodule of the span of range b with respect to B equals the span of the basis vectors, and similarly for the flipped form.

Русский

Для конечного базиса b модуля M над S дуальная подмодуля для span(range b) по B равна span(range b); аналоги для перевёрнутой формы.

LaTeX

$$$$ B.dualSubmodule(\mathrm{span}_R(\mathrm{range}\, b)) = \mathrm{span}_R(\mathrm{range}\, b). $$$$

Lean4

theorem dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) :
    B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range b))) = Submodule.span R (Set.range b) := by
  classical
  letI := FiniteDimensional.of_fintype_basis b
  rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB, dualBasis_dualBasis_flip B hB]

Похожие утверждения