Homogeneous morphisms for a shift orbit category

Mathlib's HasShift is a coherent action of an additive monoid by endofunctors. For a group action written additively, the homogeneous degree-a orbit morphisms from X to Y are the morphisms X ⟶ Y⟦a⟧. This file defines their identity and composition and proves the unit and associativity laws before passing to direct sums.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.ShiftHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] (X Y : C) (a : A) : Type v

Homogeneous orbit morphisms of degree a.

def MagnitudeConjecture.CoveringHom.shiftHomId {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) : ShiftHom X X 0

The degree-zero homogeneous identity.

noncomputable def MagnitudeConjecture.CoveringHom.shiftHomZero {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) : ShiftHom X Y 0

An ordinary morphism regarded as a degree-zero homogeneous morphism.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomZero_id {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] (X : C) : shiftHomZero (CategoryTheory.CategoryStruct.id X) = shiftHomId X

def MagnitudeConjecture.CoveringHom.shiftHomComp' {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y Z : C} {a b c : A} (h : b + a = c) (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : ShiftHom X Z c

Composition of homogeneous orbit morphisms, with an explicitly chosen output degree. The order b + a comes from applying the degree-a shift to a degree-b second morphism.

def MagnitudeConjecture.CoveringHom.shiftHomComp {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y Z : C} {a b : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : ShiftHom X Z (b + a)

Composition with its canonical output degree.

theorem MagnitudeConjecture.CoveringHom.shiftHomComp_heq_shiftHomComp' {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y Z : C} {a b c : A} (h : b + a = c) (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : shiftHomComp f g ≍ shiftHomComp' h f g

Canonical homogeneous composition agrees heterogeneously with composition at any propositionally equal output degree.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomComp'_zero_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : shiftHomComp' ⋯ (shiftHomZero f) (shiftHomZero g) = shiftHomZero (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomComp'_id_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y : C} {a : A} (f : ShiftHom X Y a) : shiftHomComp' ⋯ (shiftHomId X) f = f

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomComp'_id_right {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {X Y : C} {a : A} (f : ShiftHom X Y a) : shiftHomComp' ⋯ f (shiftHomId Y) = f

theorem MagnitudeConjecture.CoveringHom.shiftHomComp'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] {W X Y Z : C} {a b c ba cb d : A} (hba : b + a = ba) (hcb : c + b = cb) (hleft : c + ba = d) (hright : cb + a = d) (f : ShiftHom W X a) (g : ShiftHom X Y b) (h : ShiftHom Y Z c) : shiftHomComp' hleft (shiftHomComp' hba f g) h = shiftHomComp' hright f (shiftHomComp' hcb g h)

Associativity of homogeneous composition, including all degree reassociations.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.ShiftOrbitHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (A : Type w) [AddMonoid A] [CategoryTheory.HasShift C A] (X Y : C) : Type (max v w)

The finite-support direct sum of all homogeneous shift morphisms.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitOf {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] (X Y : C) (a : A) : ShiftHom X Y a →+ ShiftOrbitHom A X Y

Inclusion of one homogeneous component into the orbit Hom direct sum.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitOf_eq_directSumOf {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [DecidableEq A] (X Y : C) (a : A) (f : ShiftHom X Y a) : (shiftOrbitOf X Y a) f = (DirectSum.of (fun (c : A) => ShiftHom X Y c) a) f

With a fixed decidable equality on the degree monoid, the homogeneous inclusion is the corresponding direct-sum generator.

def MagnitudeConjecture.CoveringHom.shiftHomCompAddHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} {a b : A} : ShiftHom X Y a →+ ShiftHom Y Z b →+ ShiftHom X Z (b + a)

Homogeneous composition as a homomorphism in both variables.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomZero_smul {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] {X Y : C} (r : k) (f : X ⟶ Y) : shiftHomZero (r • f) = r • shiftHomZero f

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomComp_smul_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] {X Y Z : C} {a b : A} (r : k) (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : shiftHomComp (r • f) g = r • shiftHomComp f g

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftHomComp_smul_right {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} {a b : A} (r : k) (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : shiftHomComp f (r • g) = r • shiftHomComp f g

def MagnitudeConjecture.CoveringHom.shiftHomCompLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} {a b : A} : ShiftHom X Y a →ₗ[k] ShiftHom Y Z b →ₗ[k] ShiftHom X Z (b + a)

Homogeneous composition as a linear map in both variables.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitLof {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] (X Y : C) (a : A) : ShiftHom X Y a →ₗ[k] ShiftOrbitHom A X Y

Linear inclusion of one homogeneous component into the orbit Hom direct sum.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitLof_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] {X Y : C} {a : A} (f : ShiftHom X Y a) : (shiftOrbitLof X Y a) f = (shiftOrbitOf X Y a) f

noncomputable def MagnitudeConjecture.CoveringHom.shiftHomCompLofLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} (a b : A) : ShiftHom X Y a →ₗ[k] ShiftHom Y Z b →ₗ[k] ShiftOrbitHom A X Z

Homogeneous composition followed by inclusion in the output direct sum.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitCompLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} : ShiftOrbitHom A X Y →ₗ[k] ShiftOrbitHom A Y Z →ₗ[k] ShiftOrbitHom A X Z

Convolution as a linear map in both direct-sum variables.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitCompLinearMap_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} {a b : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : (shiftOrbitCompLinearMap ((shiftOrbitOf X Y a) f)) ((shiftOrbitOf Y Z b) g) = (shiftOrbitOf X Z (b + a)) (shiftHomComp f g)

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitCompHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} : ShiftOrbitHom A X Y →+ ShiftOrbitHom A Y Z →+ ShiftOrbitHom A X Z

Convolution composition on finite-support direct sums of homogeneous morphisms.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitCompHom_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} {a b : A} (f : ShiftHom X Y a) (g : ShiftHom Y Z b) : (shiftOrbitCompHom ((shiftOrbitOf X Y a) f)) ((shiftOrbitOf Y Z b) g) = (shiftOrbitOf X Z (b + a)) (shiftHomComp f g)

theorem MagnitudeConjecture.CoveringHom.shiftOrbitCompLinearMap_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Y Z : C} (f : ShiftOrbitHom A X Y) (g : ShiftOrbitHom A Y Z) : (shiftOrbitCompLinearMap f) g = (shiftOrbitCompHom f) g

The separately bundled bilinear convolution has the same underlying operation as the additive convolution used by the category structure.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_zero_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (shiftOrbitCompHom ((shiftOrbitOf X Y 0) (shiftHomZero f))) ((shiftOrbitOf Y Z 0) (shiftHomZero g)) = (shiftOrbitOf X Z 0) (shiftHomZero (CategoryTheory.CategoryStruct.comp f g))

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitId {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] (X : C) : ShiftOrbitHom A X X

Identity morphism in the shift-orbit Hom direct sum.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_id_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y : C} (f : ShiftOrbitHom A X Y) : (shiftOrbitCompHom (shiftOrbitId X)) f = f

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_id_right {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {X Y : C} (f : ShiftOrbitHom A X Y) : (shiftOrbitCompHom f) (shiftOrbitId Y) = f

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_assoc_of_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {W X Y Z : C} {a b c : A} (f : ShiftHom W X a) (g : ShiftHom X Y b) (h : ShiftHom Y Z c) : (shiftOrbitCompHom ((shiftOrbitCompHom ((shiftOrbitOf W X a) f)) ((shiftOrbitOf X Y b) g))) ((shiftOrbitOf Y Z c) h) = (shiftOrbitCompHom ((shiftOrbitOf W X a) f)) ((shiftOrbitCompHom ((shiftOrbitOf X Y b) g)) ((shiftOrbitOf Y Z c) h))

theorem MagnitudeConjecture.CoveringHom.shiftOrbitComp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {W X Y Z : C} (f : ShiftOrbitHom A W X) (g : ShiftOrbitHom A X Y) (h : ShiftOrbitHom A Y Z) : (shiftOrbitCompHom ((shiftOrbitCompHom f) g)) h = (shiftOrbitCompHom f) ((shiftOrbitCompHom g) h)

Associativity of convolution on the full finite-support direct sums.

def MagnitudeConjecture.CoveringHom.ShiftOrbitCategory (C : Type u) (_A : Type w) : Type u

The shift-orbit category has the same objects as C and finite-support direct sums of shifted Hom spaces as morphisms.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.categoryStruct {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : CategoryTheory.CategoryStruct.{max v w, u} (ShiftOrbitCategory C A)

@[instance_reducible]

noncomputable instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.category {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : CategoryTheory.Category.{max v w, u} (ShiftOrbitCategory C A)

noncomputable def MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.identityComponentFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : CategoryTheory.Functor C (ShiftOrbitCategory C A)

The canonical functor into the shift-orbit category, supported in degree zero on every morphism.

theorem MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.identityComponentFunctor_map_injective {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X Y : C) : Function.Injective identityComponentFunctor.map

The degree-zero component inclusion is injective on every Hom space.

theorem MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.identityComponentFunctor_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : identityComponentFunctor.Faithful

The canonical degree-zero functor is faithful without any translate orthogonality hypothesis.

@[instance_reducible]

instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.preadditive {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : CategoryTheory.Preadditive (ShiftOrbitCategory C A)

instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.identityComponentFunctor_additive {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] : identityComponentFunctor.Additive

@[instance_reducible]

instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.homModule {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] (X Y : ShiftOrbitCategory C A) : Module k (X ⟶ Y)

@[instance_reducible]

instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.linear {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Linear k (ShiftOrbitCategory C A)

instance MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.identityComponentFunctor_linear {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Functor.Linear k identityComponentFunctor