Ambient translations of normal-subgroup orbit categories #
For a normal subgroup N ≤ G, conjugation by an ambient deck translation
preserves the N-graded morphisms in the shift-orbit category. This file
constructs the resulting additive endofunctor for each g : G.
The construction embeds N-graded morphisms faithfully into the full
G-orbit category, conjugates by the canonical object-shift isomorphisms,
and projects back to subgroup degrees. Normality is used exactly to prove
that every conjugated homogeneous degree remains in N.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupProjection
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
(N : Subgroup G)
(X Y : C)
:
ShiftOrbitHom (Additive G) X Y →+ ShiftOrbitHom (Additive ↥N) X Y
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupProjection_of_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(X Y : C)
(a : Additive G)
(h : Additive.toMul a ∈ N)
(f : ShiftHom X Y a)
:
(D.shiftOrbitSubgroupProjection N X Y) ((shiftOrbitOf X Y a) f) = (shiftOrbitOf X Y (Additive.ofMul ⟨Additive.toMul a, h⟩))
((MagnitudeConjecture.CoveringHom.CoherentDeckShift.ambientShiftHomToSubgroup✝ D N X Y a h) f)
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupProjection_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(X Y : C)
(f : ShiftOrbitHom (Additive ↥N) X Y)
:
(D.shiftOrbitSubgroupProjection N X Y) ((D.shiftOrbitSubgroupMap N X Y) f) = f
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_projection_of_mem
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(X Y : C)
(a : Additive G)
(h : Additive.toMul a ∈ N)
(f : ShiftHom X Y a)
:
(D.shiftOrbitSubgroupMap N X Y) ((D.shiftOrbitSubgroupProjection N X Y) ((shiftOrbitOf X Y a) f)) = (shiftOrbitOf X Y a) f
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(X Y : C)
:
Function.Injective ⇑(D.shiftOrbitSubgroupMap N X Y)
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitAmbientConjugate
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(g : G)
{X Y : C}
(f : ShiftOrbitHom (Additive ↥N) X Y)
:
ShiftOrbitHom (Additive G) ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y)
Ambient conjugation of an N-orbit morphism by the canonical
identifications with a fixed g-shift.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitAmbientConjugate_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(g : G)
(X Y : C)
:
D.shiftOrbitAmbientConjugate N g 0 = 0
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitAmbientConjugate_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
(g : G)
{X Y : C}
(f h : ShiftOrbitHom (Additive ↥N) X Y)
:
D.shiftOrbitAmbientConjugate N g (f + h) = D.shiftOrbitAmbientConjugate N g f + D.shiftOrbitAmbientConjugate N g h
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitAmbientConjugate_homogeneous_supported
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
(X Y : C)
(a : Additive ↥N)
(f : ShiftHom X Y a)
:
(D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y))
((D.shiftOrbitSubgroupProjection N ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y))
(D.shiftOrbitAmbientConjugate N g ((shiftOrbitOf X Y a) f))) = D.shiftOrbitAmbientConjugate N g ((shiftOrbitOf X Y a) f)
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitAmbientConjugate_supported
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
{X Y : C}
(f : ShiftOrbitHom (Additive ↥N) X Y)
:
(D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y))
((D.shiftOrbitSubgroupProjection N ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y))
(D.shiftOrbitAmbientConjugate N g f)) = D.shiftOrbitAmbientConjugate N g f
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
{X Y : C}
(f : ShiftOrbitHom (Additive ↥N) X Y)
:
ShiftOrbitHom (Additive ↥N) ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y)
Translation of an N-orbit morphism by an ambient group element. It is
the subgroup-degree projection of its canonical conjugate in the full
G-orbit category.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitSubgroupMap_normalTranslateMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
{X Y : C}
(f : ShiftOrbitHom (Additive ↥N) X Y)
:
(D.shiftOrbitSubgroupMap N ((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj X)
((CategoryTheory.shiftFunctor C (Additive.ofMul g)).obj Y))
(D.shiftOrbitNormalTranslateMap N g f) = D.shiftOrbitAmbientConjugate N g f
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateMap_add
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
{X Y : C}
(f h : ShiftOrbitHom (Additive ↥N) X Y)
:
D.shiftOrbitNormalTranslateMap N g (f + h) = D.shiftOrbitNormalTranslateMap N g f + D.shiftOrbitNormalTranslateMap N g h
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
:
CategoryTheory.Functor (ShiftOrbitCategory C (Additive ↥N)) (ShiftOrbitCategory C (Additive ↥N))
The fixed ambient translation functor on the nonskeletal N-shift-orbit
category.
Instances For
instance
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitNormalTranslateFunctor_additive
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
[∀ (a : Additive G), (D.core.F a).Additive]
(N : Subgroup G)
[N.Normal]
(g : G)
:
(D.shiftOrbitNormalTranslateFunctor N g).Additive