Natural Fubini isomorphism for residual orbit push-down

For a normal subgroup N ◁ G, the iterated N- and G / N-indexed push-down value is linearly equivalent to the direct G-indexed push-down value. The equivalence uses the canonical quotient representative and the coherent addition isomorphism for deck shifts. Its compatibility with homogeneous orbit arrows extends linearly to a natural isomorphism of module functors.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupOrbitPushdownValueInclusionSummand {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) (X : C) (n : Additive ↥N) : ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj X)) →ₗ[k] orbitPushdownValue M X

Include the n-summand of subgroup push-down into the corresponding ambient-group summand.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupOrbitPushdownValueInclusion {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) (X : C) : orbitPushdownValue M X →ₗ[k] orbitPushdownValue M X

Extension by zero includes subgroup-indexed push-down values into the ambient-group push-down.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupOrbitPushdownValueInclusion_lof {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) (X : C) (n : Additive ↥N) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj X))) : (D.subgroupOrbitPushdownValueInclusion M N X) ((orbitPushdownLof M X n) x) = (orbitPushdownLof M X (Additive.ofMul ↑(Additive.toMul n))) x

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.subgroupOrbitPushdownValueInclusion_naturality {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) (X Y : C) (f : ShiftOrbitHom (Additive ↥N) X Y) : D.subgroupOrbitPushdownValueInclusion M N Y ∘ₗ (orbitPushdownMapLinear M) f = (orbitPushdownMapLinear M) ((D.shiftOrbitSubgroupMap N X Y) f) ∘ₗ D.subgroupOrbitPushdownValueInclusion M N X

Extension by zero on push-down values is natural for every subgroup orbit morphism.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualPushdownHomogeneousLinearEquiv {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (n : Additive ↥N) (X : C) : ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X))) ≃ₗ[k] ↑(M.obj ((CategoryTheory.shiftFunctor C ((normalAdditiveQuotientSubgroupEquiv N) (q, n))).obj X))

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualOrbitPushdownValueLinearEquiv {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) [N.Normal] (X : C) : (DirectSum (Additive (G ⧸ N)) fun (q : Additive (G ⧸ N)) => DirectSum (Additive ↥N) fun (n : Additive ↥N) => ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)))) ≃ₗ[k] DirectSum (Additive G) fun (g : Additive G) => ↑(M.obj ((CategoryTheory.shiftFunctor C g).obj X))

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualOrbitPushdownValueLinearEquiv_of_of {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) (M : CategoryTheory.Functor C (ModuleCat k)) (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (n : Additive ↥N) (X : C) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)))) : (D.residualOrbitPushdownValueLinearEquiv M N X) ((DirectSum.of (fun (q : Additive (G ⧸ N)) => DirectSum (Additive ↥N) fun (n : Additive ↥N) => ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)))) q) ((DirectSum.of (fun (n : Additive ↥N) => ↑(M.obj ((CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)))) n) x)) = (DirectSum.of (fun (g : Additive G) => ↑(M.obj ((CategoryTheory.shiftFunctor C g).obj X))) ((normalAdditiveQuotientSubgroupSigmaEquiv N) ⟨q, n⟩)) ((D.residualPushdownHomogeneousLinearEquiv M N q n X) x)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownResidualFubiniLinearEquiv {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) [N.Normal] (X : C) : orbitPushdownValue (orbitPushdown M) (have this := X; this) ≃ₗ[k] orbitPushdownValue M X

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownResidualFubiniIsoApp {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) [N.Normal] (X : C) : (orbitPushdown (orbitPushdown M)).obj (have this := have this := X; this; this) ≅ ((D.shiftOrbitResidualFlattenFunctor N).comp (orbitPushdown M)).obj (have this := have this := X; this; this)

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownResidualFubini_factor {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (X : C) (z : orbitPushdownValue M ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)) : (D.orbitPushdownResidualFubiniLinearEquiv M N X) ((orbitPushdownLof (orbitPushdown M) (have this := X; this) q) z) = ((orbitPushdownMapLinear M) (shiftOrbitFromShift X (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q))))) ((D.subgroupOrbitPushdownValueInclusion M N ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj X)) z)

On one quotient-degree summand, the residual Fubini equivalence is extension by zero followed by the canonical path from the chosen quotient translate.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlatten_path {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (N : Subgroup G) [N.Normal] (q r : Additive (G ⧸ N)) (n : Additive ↥N) (X Y : C) (fn : ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) : (shiftOrbitCompHom ((D.shiftOrbitSubgroupMap N (have this := (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) r).obj X; this) (have this := (CategoryTheory.shiftFunctor (ShiftOrbitCategory C (Additive ↥N)) (q + r)).obj Y; this)) (orbitPushdownArrow' ⋯ ((shiftOrbitOf X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) fn)))) (shiftOrbitFromShift Y (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul (q + r))))) = (shiftOrbitCompHom (shiftOrbitFromShift X (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul r))))) ((shiftOrbitOf X Y ((normalAdditiveQuotientSubgroupEquiv N) (q, n))) ((D.residualHomogeneousLinearEquiv N q n X Y) fn))

Flattening transports the canonical two-stage component path to the corresponding one-stage path in the ambient orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownResidualFubini_naturality {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) [N.Normal] {X Y : C} (f : (have this := X; this) ⟶ have this := Y; this) : CategoryTheory.CategoryStruct.comp ((orbitPushdown (orbitPushdown M)).map f) (D.orbitPushdownResidualFubiniIsoApp M N Y).hom = CategoryTheory.CategoryStruct.comp (D.orbitPushdownResidualFubiniIsoApp M N X).hom (((D.shiftOrbitResidualFlattenFunctor N).comp (orbitPushdown M)).map f)

The objectwise residual Fubini equivalences are natural for every finite-support morphism in the iterated orbit category.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownResidualFubiniIso {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (N : Subgroup G) [N.Normal] : orbitPushdown (orbitPushdown M) ≅ (D.shiftOrbitResidualFlattenFunctor N).comp (orbitPushdown M)

Iterated push-down along N and G / N is naturally isomorphic to direct push-down along G, after residual orbit flattening.