The Gabriel Hom equivalence for orbit push-down #
This file proves the inverse identities between finite-support homogeneous upstairs maps and transformations between their Gabriel push-down modules. The first step computes degree extraction on a single homogeneous map.
theorem
MagnitudeConjecture.CoveringHom.moduleMap_eqToHom_cast
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{I : Type w}
(P : CategoryTheory.Functor C (ModuleCat k))
(T : I → C)
{b c : I}
(h : b = c)
(x : ↑(P.obj (T c)))
:
h ▸ (CategoryTheory.ConcreteCategory.hom (P.map (CategoryTheory.eqToHom ⋯))) x = x
Mapping an equality arrow and then transporting back along the same index equality is the identity on elements.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegreeValue_map
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
(a : A)
(f : ShiftHom M₀ N₀ a)
(X : C)
(x : ↑(M₀.obj.obj X))
:
(CategoryTheory.ConcreteCategory.hom ((linearModuleShiftUnderlyingIso k D N₀ a).inv.app X))
((DirectSum.component k A (fun (b : A) => ↑(N₀.obj.obj ((D.F b).obj X))) (-a))
((shiftedOrbitPushdownValueEquiv D N₀ a X)
((orbitPushdownNatTransAppLinear f.hom X)
((orbitPushdownLof M₀.obj X 0)
((CategoryTheory.ConcreteCategory.hom (M₀.obj.map ((CategoryTheory.shiftFunctorZero C A).inv.app X)))
x))))) = (CategoryTheory.ConcreteCategory.hom (f.hom.app X)) x
Extracting degree a after descending a homogeneous degree-a map
recovers its value at every object and element.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegree_map
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
(a : A)
(f : ShiftHom M₀ N₀ a)
:
linearModuleOrbitPushdownDegree D M₀ N₀ a
(CategoryTheory.CategoryStruct.comp (linearModuleOrbitPushdown.map f)
((linearModuleOrbitPushdownCommShiftIso D a).hom.app N₀)) = f
Extraction in the same degree is a left inverse to homogeneous descent.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegree_map_ne
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
{a b : A}
(hab : b ≠ a)
(f : ShiftHom M₀ N₀ a)
:
linearModuleOrbitPushdownDegree D M₀ N₀ b
(CategoryTheory.CategoryStruct.comp (linearModuleOrbitPushdown.map f)
((linearModuleOrbitPushdownCommShiftIso D a).hom.app N₀)) = 0
Extraction in any other degree vanishes after homogeneous descent.
noncomputable def
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownSynthesisLinear
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
:
ShiftOrbitHom A M₀ N₀ →ₗ[k] linearModuleOrbitPushdown.obj M₀ ⟶ linearModuleOrbitPushdown.obj N₀
The linear synthesis map in Gabriel's Hom formula.
Instances For
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownSynthesisLinear_comp
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M N Z : LinearModuleCategory k)
(f : ShiftOrbitHom A M N)
(g : ShiftOrbitHom A N Z)
:
CategoryTheory.CategoryStruct.comp ((linearModuleOrbitPushdownSynthesisLinear D M N) f)
((linearModuleOrbitPushdownSynthesisLinear D N Z) g) = (linearModuleOrbitPushdownSynthesisLinear D M Z) ((shiftOrbitCompHom f) g)
Synthesis in Gabriel's Hom formula respects shift-orbit convolution.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownSynthesisLinear_zero
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
(f : M₀ ⟶ N₀)
:
(linearModuleOrbitPushdownSynthesisLinear D M₀ N₀) ((shiftOrbitOf M₀ N₀ 0) (shiftHomZero f)) = linearModuleOrbitPushdown.map f
On the degree-zero inclusion of an ordinary upstairs map, synthesis is exactly the original push-down functor map.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegrees_synthesis
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
(f : ShiftOrbitHom A M₀.obj N₀)
:
linearModuleOrbitPushdownDegrees D M₀ N₀ ((linearModuleOrbitPushdownSynthesisLinear D M₀.obj N₀) f) = f
Extracting all degrees after synthesis recovers a finite-support orbit morphism.
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownFromShift_zero_lof
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M : CategoryTheory.Functor C (ModuleCat k))
[M.Additive]
[CategoryTheory.Functor.Linear k M]
(X : C)
(b : A)
(x : ↑(M.obj ((D.F b).obj X)))
:
((orbitPushdownMapLinear M) (shiftOrbitFromShift X b))
((orbitPushdownLof M ((D.F b).obj X) 0)
((CategoryTheory.ConcreteCategory.hom (M.map (D.zero.inv.app ((D.F b).obj X)))) x)) = (orbitPushdownLof M X b) x
The canonical orbit arrow from a shifted object sends its normalized degree-zero inclusion to the corresponding homogeneous inclusion.
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_ext_zero
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
{M N : CategoryTheory.Functor C (ModuleCat k)}
[M.Additive]
[CategoryTheory.Functor.Linear k M]
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(α β : orbitPushdown M ⟶ orbitPushdown N)
:
(∀ (X : C) (x : ↑(M.obj X)),
(CategoryTheory.ConcreteCategory.hom (α.app X))
((orbitPushdownLof M X 0)
((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) x)) = (CategoryTheory.ConcreteCategory.hom (β.app X))
((orbitPushdownLof M X 0)
((CategoryTheory.ConcreteCategory.hom (M.map ((CategoryTheory.shiftFunctorZero C A).inv.app X))) x))) →
α = β
A transformation between orbit push-downs is determined by its values on the normalized degree-zero inclusions at all upstairs objects.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegree_jointlyFaithful
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ N₀ : LinearModuleCategory k)
(α β : linearModuleOrbitPushdown.obj M₀ ⟶ linearModuleOrbitPushdown.obj N₀)
:
(∀ (a : A), linearModuleOrbitPushdownDegree D M₀ N₀ a α = linearModuleOrbitPushdownDegree D M₀ N₀ a β) → α = β
The extracted shifted degree maps jointly determine a transformation between orbit push-down modules.
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownSynthesis_degrees
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
(α : linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀)
:
(linearModuleOrbitPushdownSynthesisLinear D M₀.obj N₀) (linearModuleOrbitPushdownDegrees D M₀ N₀ α) = α
Synthesizing the extracted degrees recovers the original push-down transformation.
noncomputable def
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownHomLinearEquiv
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
:
ShiftOrbitHom A M₀.obj N₀ ≃ₗ[k] linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀
Gabriel's Hom formula for the orbit push-down: finite-support shifted upstairs maps are linearly equivalent to transformations downstairs.