Linear Fubini equivalences for residual orbit flattening

For a normal subgroup N ◁ G, multiplication identifies (G / N) × N with G after choosing the canonical quotient representatives. This file lifts that bijection to the homogeneous shifted Hom spaces and their finite-support direct sums. It also records the corresponding formula for the actual residual flattening functor on a doubly homogeneous generator.

noncomputable def normalQuotientSubgroupEquiv {G : Type w} [Group G] (N : Subgroup G) [N.Normal] : (G ⧸ N) × ↥N ≃ G

@[simp]

theorem normalQuotientSubgroupEquiv_apply {G : Type w} [Group G] (N : Subgroup G) [N.Normal] (q : G ⧸ N) (n : ↥N) : (normalQuotientSubgroupEquiv N) (q, n) = MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative N q * ↑n

noncomputable def normalAdditiveQuotientSubgroupEquiv {G : Type w} [Group G] (N : Subgroup G) [N.Normal] : Additive (G ⧸ N) × Additive ↥N ≃ Additive G

@[simp]

theorem normalAdditiveQuotientSubgroupEquiv_apply {G : Type w} [Group G] (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (n : Additive ↥N) : (normalAdditiveQuotientSubgroupEquiv N) (q, n) = Additive.ofMul (MagnitudeConjecture.CoveringHom.CoherentDeckShift.normalQuotientRepresentative N (Additive.toMul q) * ↑(Additive.toMul n))

noncomputable def normalAdditiveQuotientSubgroupSigmaEquiv {G : Type w} [Group G] (N : Subgroup G) [N.Normal] : (_ : Additive (G ⧸ N)) × Additive ↥N ≃ Additive G

@[simp]

theorem normalAdditiveQuotientSubgroupSigmaEquiv_apply {G : Type w} [Group G] (N : Subgroup G) [N.Normal] (p : (_ : Additive (G ⧸ N)) × Additive ↥N) : (normalAdditiveQuotientSubgroupSigmaEquiv N) p = (normalAdditiveQuotientSubgroupEquiv N) (p.fst, p.snd)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualHomogeneousLinearEquiv {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) (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (n : Additive ↥N) (X Y : C) : ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n ≃ₗ[k] ShiftHom X Y ((normalAdditiveQuotientSubgroupSigmaEquiv N) ⟨q, n⟩)

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_map_of_of {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 : Additive (G ⧸ N)) (n : Additive ↥N) (X Y : C) (f : ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) : (D.shiftOrbitResidualFlattenFunctor N).map ((shiftOrbitOf (have this := X; this) (have this := Y; this) q) ((shiftOrbitOf X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) f)) = (shiftOrbitOf X Y ((normalAdditiveQuotientSubgroupEquiv N) (q, n))) ((D.residualHomogeneousLinearEquiv N q n X Y) f)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualFlattenUncurryLinearEquiv {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) (N : Subgroup G) [N.Normal] (X Y : C) : (DirectSum (Additive (G ⧸ N)) fun (q : Additive (G ⧸ N)) => DirectSum (Additive ↥N) fun (n : Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) ≃ₗ[k] DirectSum ((_ : Additive (G ⧸ N)) × Additive ↥N) fun (p : (_ : Additive (G ⧸ N)) × Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul p.fst)))).obj Y) p.snd

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualFlattenFiberwiseLinearEquiv {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) (N : Subgroup G) [N.Normal] (X Y : C) : (DirectSum ((_ : Additive (G ⧸ N)) × Additive ↥N) fun (p : (_ : Additive (G ⧸ N)) × Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul p.fst)))).obj Y) p.snd) ≃ₗ[k] DirectSum ((_ : Additive (G ⧸ N)) × Additive ↥N) fun (p : (_ : Additive (G ⧸ N)) × Additive ↥N) => ShiftHom X Y ((normalAdditiveQuotientSubgroupSigmaEquiv N) p)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualFlattenDegreeLinearEquiv {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) (N : Subgroup G) [N.Normal] (X Y : C) : (DirectSum ((_ : Additive (G ⧸ N)) × Additive ↥N) fun (p : (_ : Additive (G ⧸ N)) × Additive ↥N) => ShiftHom X Y ((normalAdditiveQuotientSubgroupSigmaEquiv N) p)) ≃ₗ[k] DirectSum (Additive G) fun (g : Additive G) => ShiftHom X Y g

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualFlattenDirectSumLinearEquiv {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) (N : Subgroup G) [N.Normal] (X Y : C) : (DirectSum (Additive (G ⧸ N)) fun (q : Additive (G ⧸ N)) => DirectSum (Additive ↥N) fun (n : Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) ≃ₗ[k] DirectSum (Additive G) fun (g : Additive G) => ShiftHom X Y g

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.residualFlattenDirectSumLinearEquiv_of_of {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) (N : Subgroup G) [N.Normal] (q : Additive (G ⧸ N)) (n : Additive ↥N) (X Y : C) (f : ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) : (D.residualFlattenDirectSumLinearEquiv N X Y) ((DirectSum.of (fun (q : Additive (G ⧸ N)) => DirectSum (Additive ↥N) fun (n : Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) q) ((DirectSum.of (fun (n : Additive ↥N) => ShiftHom X ((CategoryTheory.shiftFunctor C (Additive.ofMul (normalQuotientRepresentative N (Additive.toMul q)))).obj Y) n) n) f)) = (DirectSum.of (fun (g : Additive G) => ShiftHom X Y g) ((normalAdditiveQuotientSubgroupSigmaEquiv N) ⟨q, n⟩)) ((D.residualHomogeneousLinearEquiv N q n X Y) f)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenHomLinearEquiv {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] (X Y : C) : ((have this := have this := X; this; this) ⟶ have this := have this := Y; this; this) ≃ₗ[k] (have this := X; this) ⟶ have this := Y; this

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenHomLinearEquiv_toLinearMap {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] (X Y : C) : ↑(D.shiftOrbitResidualFlattenHomLinearEquiv N X Y) = CategoryTheory.Functor.mapLinearMap k (D.shiftOrbitResidualFlattenFunctor N)

The Fubini equivalence on residual-orbit Hom spaces is the linear map of the actual residual flattening functor.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_map_bijective {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] (X Y : C) : Function.Bijective (D.shiftOrbitResidualFlattenFunctor N).map

Residual orbit flattening is bijective on every Hom space.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_full {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] : (D.shiftOrbitResidualFlattenFunctor N).Full

Residual orbit flattening is full.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitResidualFlattenFunctor_faithful {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] : (D.shiftOrbitResidualFlattenFunctor N).Faithful

Residual orbit flattening is faithful.