OAI/Algebra/Finitistic/Localization/FiniteSupportReindex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.FiniteSupportReindex.coefficient line 15

    Source documentation

    Extend a finite family of actual components by zero in every other degree.

    def coefficient (n : ℤ) : (∀ i, V (p i)) →ₗ[R] V n := by
…
  2. theorem OAI.LittleFinitistic.FiniteSupportReindex.coefficient_at line 21
  3. theorem OAI.LittleFinitistic.FiniteSupportReindex.coefficient_outside line 33
  4. def OAI.LittleFinitistic.FiniteSupportReindex.reindex line 38

    Source documentation

    Read the same family using another finite set of support degrees.

    def reindex : (∀ i, V (p i)) →ₗ[R] (∀ j, V (q j)) :=
…
  5. theorem OAI.LittleFinitistic.FiniteSupportReindex.reindex_apply line 41
  6. theorem OAI.LittleFinitistic.FiniteSupportReindex.coefficient_reindex line 44
  7. def OAI.LittleFinitistic.FiniteSupportReindex.equivalence line 57

    Source documentation

    Changing finite support indices adds or removes only zero terms. The maps are the actual coordinate inclusions/projections, including all degree transports.

    def equivalence (hp : Function.Injective p) (hq : Function.Injective q)
    (hVp : ∀ n, (∀ i, p i ≠ n) → IsZero (V n))
    (hVq : ∀ n, (∀ j, q j ≠ n) → IsZero (V n)) :
    (∀ i, V (p i)) ≃ₗ[R] (∀ j, V (q j)) where
…