Orbit push-down of representable modules #
Gabriel push-down sends the covariant linear representable at an upstairs object to the covariant linear representable at the same object in the shift-orbit category. This is the projective half of the Nakayama comparison used in preservation of Auslander--Reiten sequences.
instance
MagnitudeConjecture.CoveringHom.linearCoyoneda_obj_linear
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(X : C)
:
CategoryTheory.Functor.Linear k ((CategoryTheory.linearCoyoneda k C).obj (Opposite.op X))
noncomputable def
MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModule
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(X : C)
:
The covariant linear representable as an object of the full category of additive linear modules.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModuleMap
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Z : C}
(f : X ⟶ Z)
:
A morphism of representing objects induces the contravariant map between the corresponding projective representables.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyoneda
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(X : C)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
A representable known to have finite support and finite-dimensional values, bundled in the finite-dimensional module category.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaMap
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{X Z : C}
(f : X ⟶ Z)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hZ : IsFiniteDimensionalModule k (linearCoyonedaLinearModule Z))
:
Finite-dimensional bundled form of the map between projective representables induced by a representing morphism.
Instances For
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownLinearCoyoneda_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]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)]
(X Y Z : C)
(f : ShiftOrbitHom A Y Z)
:
(orbitPushdownMapLinear ((CategoryTheory.linearCoyoneda k C).obj (Opposite.op X))) f = shiftOrbitCompLinearMap.flip f
On a representable module, the push-down action is right composition in the shift-orbit category.
noncomputable def
MagnitudeConjecture.CoveringHom.orbitPushdownLinearCoyonedaIso
{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]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)]
(X : C)
:
orbitPushdown ((CategoryTheory.linearCoyoneda k C).obj (Opposite.op X)) ≅ (CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C A)).obj
(Opposite.op
(have this := X;
this))
Orbit push-down of Hom(X,-) is the representable module
Hom_orbit(X,-).
Instances For
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownLinearCoyonedaIso_representing_naturality
{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]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)]
{X Z : C}
(f : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans ((CategoryTheory.linearCoyoneda k C).map f.op))
(orbitPushdownLinearCoyonedaIso X).hom = CategoryTheory.CategoryStruct.comp (orbitPushdownLinearCoyonedaIso Z).hom
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C A)).map
(ShiftOrbitCategory.identityComponentFunctor.map f).op)
The representable push-down isomorphisms commute with morphisms of representing objects.
noncomputable def
MagnitudeConjecture.CoveringHom.deckOrbitRepresentativeLinearCoyonedaIso
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.HasShift C (Additive G)]
[∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)]
(q : MulAction.orbitRel.Quotient G C)
:
deckOrbitRepresentativeFunctor.comp
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).obj
(Opposite.op
(have this := deckOrbitRepresentative q;
this))) ≅ (CategoryTheory.linearCoyoneda k (DeckOrbitSkeleton C G)).obj (Opposite.op q)
Restricting the orbit representable at a chosen representative gives the literal representable on the induced orbit skeleton.
Instances For
theorem
MagnitudeConjecture.CoveringHom.deckOrbitRepresentativeLinearCoyonedaIso_representing_naturality
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{G : Type w}
[Group G]
[MulAction G C]
[CategoryTheory.HasShift C (Additive G)]
[∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)]
{q r : MulAction.orbitRel.Quotient G C}
(f :
(have this := q;
this) ⟶ have this := r;
this)
:
CategoryTheory.CategoryStruct.comp
(deckOrbitRepresentativeFunctor.whiskerLeft
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).map
(deckOrbitRepresentativeFunctor.map f).op))
(deckOrbitRepresentativeLinearCoyonedaIso q).hom = CategoryTheory.CategoryStruct.comp (deckOrbitRepresentativeLinearCoyonedaIso r).hom
((CategoryTheory.linearCoyoneda k (DeckOrbitSkeleton C G)).map f.op)
Restriction to the chosen orbit skeleton commutes with morphisms of representing objects for projective representables.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearCoyonedaMap_objectIsoDeckOrbitRepresentative_naturality
{k : Type uK}
[Field 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)]
{X Z : C}
(f : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).map
(ShiftOrbitCategory.identityComponentFunctor.map f).op)
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).mapIso
(D.objectIsoDeckOrbitRepresentative X).symm.op).hom = CategoryTheory.CategoryStruct.comp
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).mapIso
(D.objectIsoDeckOrbitRepresentative Z).symm.op).hom
((CategoryTheory.linearCoyoneda k (ShiftOrbitCategory C (Additive G))).map
(deckOrbitRepresentativeFunctor.map (D.orbitSkeletonMap f)).op)
Moving projective representables to chosen orbit representatives commutes with the induced morphism between those representatives.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownLinearCoyonedaIso
{k : Type uK}
[Field 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)]
(X : C)
:
orbitSkeletonPushdown ((CategoryTheory.linearCoyoneda k C).obj (Opposite.op X)) ≅ (CategoryTheory.linearCoyoneda k (DeckOrbitSkeleton C G)).obj (Opposite.op (Quotient.mk'' X))
Skeletal Gabriel push-down sends the projective representable at X to
the projective representable at the strict orbit of X.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownLinearCoyonedaIso_representing_naturality
{k : Type uK}
[Field 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)]
{X Z : C}
(f : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(deckOrbitRepresentativeFunctor.whiskerLeft (orbitPushdownNatTrans ((CategoryTheory.linearCoyoneda k C).map f.op)))
(D.orbitSkeletonPushdownLinearCoyonedaIso X).hom = CategoryTheory.CategoryStruct.comp (D.orbitSkeletonPushdownLinearCoyonedaIso Z).hom
((CategoryTheory.linearCoyoneda k (DeckOrbitSkeleton C G)).map (D.orbitSkeletonMap f).op)
The skeletal projective-representable isomorphisms commute with the morphism between strict deck orbits induced by an upstairs morphism.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso
{k : Type uK}
[Field 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)]
(X : C)
:
linearModuleOrbitSkeletonPushdown.obj (linearCoyonedaLinearModule X) ≅ linearCoyonedaLinearModule (Quotient.mk'' X)
Bundled linear-module form of skeletal push-down preserving projective representables.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso_hom_hom
{k : Type uK}
[Field 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)]
(X : C)
:
(D.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso X).hom.hom = (D.orbitSkeletonPushdownLinearCoyonedaIso X).hom
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso_representing_naturality
{k : Type uK}
[Field 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)]
{X Z : C}
(f : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (linearModuleOrbitSkeletonPushdown.map (linearCoyonedaLinearModuleMap f))
(D.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso X).hom = CategoryTheory.CategoryStruct.comp (D.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso Z).hom
(linearCoyonedaLinearModuleMap (D.orbitSkeletonMap f))
The skeletal projective comparison is natural in the representing object inside the category of additive linear modules.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalLinearCoyoneda
{k : Type uK}
[Field 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)]
[IsCancelSMul G C]
(X : C)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
The orbit-skeleton representable, with finiteness transported from an upstairs finite representable through finite skeletal push-down.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalLinearCoyonedaMap
{k : Type uK}
[Field 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)]
[IsCancelSMul G C]
{X Z : C}
(f : X ⟶ Z)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hZ : IsFiniteDimensionalModule k (linearCoyonedaLinearModule Z))
:
The finite-dimensional skeletal projective representables inherit the map induced by a morphism of upstairs representing objects.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso
{k : Type uK}
[Field 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)]
[IsCancelSMul G C]
(X : C)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
Literal finite-dimensional push-down preserves a finite projective representable.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso_hom_hom
{k : Type uK}
[Field 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)]
[IsCancelSMul G C]
(X : C)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
(D.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso X hX).hom.hom = (D.linearModuleOrbitSkeletonPushdownLinearCoyonedaIso X).hom
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso_representing_naturality
{k : Type uK}
[Field 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)]
[IsCancelSMul G C]
{X Z : C}
(f : X ⟶ Z)
(hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hZ : IsFiniteDimensionalModule k (linearCoyonedaLinearModule Z))
:
CategoryTheory.CategoryStruct.comp
(D.finiteDimensionalModuleOrbitSkeletonPushdown.map (finiteDimensionalLinearCoyonedaMap f hX hZ))
(D.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (D.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso Z hZ).hom
(D.orbitSkeletonFiniteDimensionalLinearCoyonedaMap f hX hZ)
Literal finite-dimensional skeletal push-down preserves the morphisms between finite projective representables.