Module equivalences over strict orbit towers #
A linear equivalence of base categories acts on covariant linear modules by precomposition. If its object map is a literal bijection, this equivalence restricts further to modules with finite object support. Applied to strict orbit-tower flattening, this identifies the linear and finite-dimensional module categories over the two-stage and direct orbit skeletons.
noncomputable def
MagnitudeConjecture.CoveringHom.linearModuleCongrEquivalence
{R : Type uK}
[CommRing R]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear R e.functor]
:
Precomposition with the forward functor of a linear equivalence induces an equivalence from linear modules on the target to linear modules on the source.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.linearModuleCongrEquivalence_functor_obj_obj
{R : Type uK}
[CommRing R]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear R e.functor]
(M : LinearModuleCategory R)
:
((linearModuleCongrEquivalence e).functor.obj M).obj = e.functor.comp M.obj
instance
MagnitudeConjecture.CoveringHom.linearModuleCongrEquivalence_functor_additive
{R : Type uK}
[CommRing R]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear R e.functor]
:
(linearModuleCongrEquivalence e).functor.Additive
instance
MagnitudeConjecture.CoveringHom.linearModuleCongrEquivalence_functor_linear
{R : Type uK}
[CommRing R]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear R e.functor]
:
CategoryTheory.Functor.Linear R (linearModuleCongrEquivalence e).functor
noncomputable def
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalence
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
(eobj : C ≃ D)
(hobj : ∀ (X : C), e.functor.obj X = eobj X)
:
If the forward functor of a linear equivalence has a specified bijective object map, precomposition restricts to an equivalence of finite-dimensional modules with finite literal object support.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalenceOfFinite
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
[Finite C]
[Finite D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
:
Over finite object types, every literal object support is finite, so an arbitrary linear equivalence of base categories induces an equivalence of finite-dimensional module categories without choosing a bijection of object types.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalence_functor_obj_obj_obj
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
(eobj : C ≃ D)
(hobj : ∀ (X : C), e.functor.obj X = eobj X)
(M : FiniteDimensionalModuleCategory k)
:
((finiteDimensionalModuleCongrEquivalence e eobj hobj).functor.obj M).obj.obj = e.functor.comp M.obj.obj
instance
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalence_functor_additive
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
(eobj : C ≃ D)
(hobj : ∀ (X : C), e.functor.obj X = eobj X)
:
(finiteDimensionalModuleCongrEquivalence e eobj hobj).functor.Additive
instance
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalence_functor_linear
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
(eobj : C ≃ D)
(hobj : ∀ (X : C), e.functor.obj X = eobj X)
:
CategoryTheory.Functor.Linear k (finiteDimensionalModuleCongrEquivalence e eobj hobj).functor
instance
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalenceOfFinite_functor_additive
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
[Finite C]
[Finite D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
:
(finiteDimensionalModuleCongrEquivalenceOfFinite e).functor.Additive
instance
MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCongrEquivalenceOfFinite_functor_linear
{k : Type uK}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
[Finite C]
[Finite D]
(e : C ≌ D)
[e.functor.Additive]
[CategoryTheory.Functor.Linear k e.functor]
:
CategoryTheory.Functor.Linear k (finiteDimensionalModuleCongrEquivalenceOfFinite e).functor
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerLinearModuleEquivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
{R : Type uK}
[CommRing R]
[CategoryTheory.Linear R C]
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear R (D.core.F a)]
(N : Subgroup G)
[N.Normal]
:
Linear modules over the direct strict orbit skeleton are equivalent to linear modules over the two-stage strict orbit skeleton.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitTowerFiniteDimensionalModuleEquivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{G : Type w}
[Group G]
[MulAction G C]
(D : CoherentDeckShift C G)
{k : Type uK}
[Field k]
[CategoryTheory.Linear k C]
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)]
(N : Subgroup G)
[N.Normal]
:
Finite-dimensional modules over the direct strict orbit skeleton are equivalent to finite-dimensional modules over the two-stage strict orbit skeleton.