Reversing a genuine finite right-ladder window over Fin.rev

This file is a pure dependent-reindexing adapter. It introduces no new representation-theoretic or concrete-module input.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.familyHom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : ℕ → C) (b : (k : ℕ) → F k ⟶ G k) {m n : ℕ} (e : m = n) : CategoryTheory.CategoryStruct.comp (b m) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (b n)

A family of morphisms commutes with transport of its index.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.transported_right_rung_comm {C : Type u} [CategoryTheory.Category.{v, u} C] (Y Z : ℕ → C) (b : (k : ℕ) → Z k ⟶ Y k) {a c j : ℕ} (ea : a = j + 1) (ec : j = c) (f : Y (j + 1) ⟶ Y j) (g : Z (j + 1) ⟶ Z j) (comm : CategoryTheory.CategoryStruct.comp (b (j + 1)) f = CategoryTheory.CategoryStruct.comp g (b j)) : CategoryTheory.CategoryStruct.comp (b a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯))) (b c)

Transport the connecting square of one genuine right-ladder rung from indices j+1 → j to propositionally equal indices a → c.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.transported_right_rung_hzero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y Z U : ℕ → C) (b : (k : ℕ) → Z k ⟶ Y k) {a c j : ℕ} (ea : a = j + 1) (ec : j = c) (h : U (j + 1) ⟶ Z j) (hzero : CategoryTheory.CategoryStruct.comp h (b j) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp h (CategoryTheory.eqToHom ⋯))) (b c) = 0

Transport the zero relation for the complementary map of one genuine right-ladder rung.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.transported_right_step_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (Y Z U : ℕ → C) (b : (k : ℕ) → Z k ⟶ Y k) {a c j : ℕ} (ea : a = j + 1) (ec : j = c) (f : Y (j + 1) ⟶ Y j) (g : Z (j + 1) ⟶ Z j) (h : U (j + 1) ⟶ Z j) (comm : CategoryTheory.CategoryStruct.comp (b (j + 1)) f = CategoryTheory.CategoryStruct.comp g (b j)) (hzero : CategoryTheory.CategoryStruct.comp h (b j) = 0) : RightLadder.stepComplex (b j) (b (j + 1)) f g h comm hzero ≅ RightLadder.stepComplex (b c) (b a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp h (CategoryTheory.eqToHom ⋯))) ⋯ ⋯

The explicit right-step complex is invariant, up to componentwise equality isomorphisms, under transport of its two endpoint indices.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.ofInfiniteSpecialRightLadder {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) : ReversedRightPrefix T n

Restrict an actual infinite special right ladder to its first n+1 arrows and reverse that finite window using Fin.rev.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.ofInfiniteSpecialRightLadder_stepIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (i : Fin n) : RightLadder.stepComplex (R.b ↑i.rev) (R.b (↑i.rev + 1)) (R.f ↑i.rev) (R.g ↑i.rev) (R.h ↑i.rev) ⋯ ⋯ ≅ RightLadder.stepComplex ((ofInfiniteSpecialRightLadder R n).b i.succ) ((ofInfiniteSpecialRightLadder R n).b i.castSucc) ((ofInfiniteSpecialRightLadder R n).f i) ((ofInfiniteSpecialRightLadder R n).g i) ((ofInfiniteSpecialRightLadder R n).h i) ⋯ ⋯

The displayed rung of the reversed prefix is the corresponding genuine right-ladder rung, transported across the two Fin.rev index equalities.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ReversedRightPrefix.ofInfiniteSpecialRightLadder_paddedArrowIso_last {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) : CategoryTheory.Arrow.mk ((ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.biprod.desc (R.b 0) 0)

The last padded arrow of a reversed finite window is the initial padded arrow of the original right ladder.