Pullback decompositions along a linear covering

Restriction of a covariant linear module along a linear functor is again a linear module. For a covering functor, the pullback of a representable is the direct sum of the representables indexed by the fixed source fibre.

The fixed-fibre formulation is important: the indexing objects do not move with the variable of the module, so the covering Hom equivalence is genuinely natural without any choice of deck transformations.

theorem MagnitudeConjecture.LinearCovering.finite_nontrivial_of_finiteDimensional_directSum {k : Type u} [Field k] {ι : Type} (V : ι → Type u) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [FiniteDimensional k (DirectSum ι V)] : {i : ι | Nontrivial (V i)}.Finite

A finite-dimensional direct sum has only finitely many nontrivial summands.

theorem MagnitudeConjecture.LinearCovering.directSum_subsingleton_of_not_nonempty {ι : Type} (V : ι → Type u) [(i : ι) → AddCommGroup (V i)] (hι : ¬Nonempty ι) : Subsingleton (DirectSum ι V)

A direct sum indexed by an empty type has at most one element.

theorem MagnitudeConjecture.LinearCovering.IsCovering.targetHom_subsingleton_of_fiber_not_nonempty {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : C) (Y : D) (hY : ¬Nonempty (Fiber F Y)) : Subsingleton (F.obj X ⟶ Y)

If the target fibre is empty, every morphism from an object in the image of a covering to that target is zero.

theorem MagnitudeConjecture.LinearCovering.IsCovering.sourceHom_subsingleton_of_fiber_not_nonempty {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) (Y : C) (hX : ¬Nonempty (Fiber F X)) : Subsingleton (X ⟶ F.obj Y)

If the source fibre is empty, every morphism from that source to an object in the image of a covering is zero.

noncomputable def MagnitudeConjecture.LinearCovering.linearModulePullback {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (M : CoveringHom.LinearModuleCategory k) : CoveringHom.LinearModuleCategory k

Restriction of a covariant linear module along a linear functor.

noncomputable def MagnitudeConjecture.LinearCovering.linearModulePullbackIso {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] {M N : CoveringHom.LinearModuleCategory k} (e : M ≅ N) : linearModulePullback F M ≅ linearModulePullback F N

Restriction along a linear functor preserves isomorphisms of linear modules.

noncomputable def MagnitudeConjecture.LinearCovering.sourceFiberRepresentableSum {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CategoryTheory.Functor C (ModuleCat k)

The fixed-source-fibre direct sum of representables. At Y its value is ⨁_(P in F⁻¹(X)) Hom(P,Y).

instance MagnitudeConjecture.LinearCovering.sourceFiberRepresentableSum_additive {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : (sourceFiberRepresentableSum F X).Additive

instance MagnitudeConjecture.LinearCovering.sourceFiberRepresentableSum_linear {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CategoryTheory.Functor.Linear k (sourceFiberRepresentableSum F X)

noncomputable def MagnitudeConjecture.LinearCovering.sourceFiberRepresentableLinearModule {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CoveringHom.LinearModuleCategory k

The fixed-source-fibre sum, bundled in the category of linear modules.

noncomputable def MagnitudeConjecture.LinearCovering.sourceFiberRepresentableInclusion {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (P : Fiber F X) : CoveringHom.linearCoyonedaLinearModule ↑P ⟶ sourceFiberRepresentableLinearModule F X

Include one representable indexed by the fixed source fibre into the direct-sum module.

noncomputable def MagnitudeConjecture.LinearCovering.sourceFiberRepresentableProjection {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (P : Fiber F X) : sourceFiberRepresentableLinearModule F X ⟶ CoveringHom.linearCoyonedaLinearModule ↑P

Project the fixed-source direct-sum module onto one representable summand.

theorem MagnitudeConjecture.LinearCovering.sourceFiberRepresentableInclusion_projection {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (P : Fiber F X) : CategoryTheory.CategoryStruct.comp (sourceFiberRepresentableInclusion F X P) (sourceFiberRepresentableProjection F X P) = CategoryTheory.CategoryStruct.id (CoveringHom.linearCoyonedaLinearModule ↑P)

theorem MagnitudeConjecture.LinearCovering.sourceFiberRepresentableInclusion_projection_assoc {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (P : Fiber F X) {Z : CoveringHom.LinearModuleCategory k} (h : CoveringHom.linearCoyonedaLinearModule ↑P ⟶ Z) : CategoryTheory.CategoryStruct.comp (sourceFiberRepresentableInclusion F X P) (CategoryTheory.CategoryStruct.comp (sourceFiberRepresentableProjection F X P) h) = h

noncomputable def MagnitudeConjecture.LinearCovering.sourceFiberRepresentablePullbackIso {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) : sourceFiberRepresentableLinearModule F X ≅ linearModulePullback F (CoveringHom.linearCoyonedaLinearModule X)

A covering identifies the fixed-source-fibre representable sum with the pullback of the downstairs representable.

def MagnitudeConjecture.LinearCovering.targetFiberDualMap {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) {Y Z : C} (f : Y ⟶ Z) : (DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Y ⟶ ↑J)) →ₗ[k] DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Z ⟶ ↑J)

On the duals of the fixed-target-fibre Hom spaces, a morphism acts componentwise by dualized precomposition.

@[simp]

theorem MagnitudeConjecture.LinearCovering.targetFiberDualMap_apply {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) {Y Z : C} (f : Y ⟶ Z) (a : DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Y ⟶ ↑J)) (J : Fiber F X) : ((targetFiberDualMap F X f) a) J = (CategoryTheory.Linear.leftComp k (↑J) f).dualMap (a J)

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableSum {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CategoryTheory.Functor C (ModuleCat k)

The fixed-target-fibre direct sum of dual corepresentables. At Y its value is ⨁_(J in F⁻¹(X)) D Hom(Y,J).

instance MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableSum_additive {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : (targetFiberDualCorepresentableSum F X).Additive

instance MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableSum_linear {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CategoryTheory.Functor.Linear k (targetFiberDualCorepresentableSum F X)

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableLinearModule {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) : CoveringHom.LinearModuleCategory k

The fixed-target-fibre dual-corepresentable sum, bundled as a linear module.

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableInclusion {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (J : Fiber F X) : CoveringHom.dualLinearYonedaLinearModule ↑J ⟶ targetFiberDualCorepresentableLinearModule F X

Include one dual corepresentable indexed by the fixed target fibre into the direct-sum module.

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableProjection {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (J : Fiber F X) : targetFiberDualCorepresentableLinearModule F X ⟶ CoveringHom.dualLinearYonedaLinearModule ↑J

Project the fixed-target direct-sum module onto one dual corepresentable summand.

theorem MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableInclusion_projection {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (J : Fiber F X) : CategoryTheory.CategoryStruct.comp (targetFiberDualCorepresentableInclusion F X J) (targetFiberDualCorepresentableProjection F X J) = CategoryTheory.CategoryStruct.id (CoveringHom.dualLinearYonedaLinearModule ↑J)

theorem MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableInclusion_projection_assoc {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) (J : Fiber F X) {Z : CoveringHom.LinearModuleCategory k} (h : CoveringHom.dualLinearYonedaLinearModule ↑J ⟶ Z) : CategoryTheory.CategoryStruct.comp (targetFiberDualCorepresentableInclusion F X J) (CategoryTheory.CategoryStruct.comp (targetFiberDualCorepresentableProjection F X J) h) = h

theorem MagnitudeConjecture.LinearCovering.targetFiberLof_eq_directSumInclusion {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : C) (Y : D) (J : Fiber F Y) : targetFiberLof F X Y J = directSumInclusion (fun (L : Fiber F Y) => X ⟶ ↑L) J

The covering-specific inclusion agrees with the canonical direct-sum inclusion, independently of the hidden decidable-equality choice.

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableValueEquiv {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) (Y : C) (hfinite : {J : Fiber F X | Nontrivial (Y ⟶ ↑J)}.Finite) : (DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Y ⟶ ↑J)) ≃ₗ[k] Module.Dual k (F.obj Y ⟶ X)

Pointwise, finite direct-sum duality followed by the dual covering Hom equivalence identifies the fixed-target sum with the dual Hom space downstairs.

@[simp]

theorem MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentableValueEquiv_apply {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) (Y : C) (hfinite : {J : Fiber F X | Nontrivial (Y ⟶ ↑J)}.Finite) (a : DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Y ⟶ ↑J)) (q : F.obj Y ⟶ X) : ((targetFiberDualCorepresentableValueEquiv F hF X Y hfinite) a) q = ((directSumDualToDual fun (J : Fiber F X) => Y ⟶ ↑J) a) ((hF.targetFiberHomLinearEquiv Y X).symm q)

theorem MagnitudeConjecture.LinearCovering.targetFiberHomLinearEquiv_symm_comp {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) {Y Z : C} (f : Y ⟶ Z) (q : F.obj Z ⟶ X) : (hF.targetFiberHomLinearEquiv Y X).symm (CategoryTheory.CategoryStruct.comp (F.map f) q) = (targetFiberPrecomp F X f) ((hF.targetFiberHomLinearEquiv Z X).symm q)

The inverse covering Hom equivalences commute with precomposition.

theorem MagnitudeConjecture.LinearCovering.targetFiberDualMap_pairing {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (F : CategoryTheory.Functor C D) (X : D) {Y Z : C} (f : Y ⟶ Z) (a : DirectSum (Fiber F X) fun (J : Fiber F X) => Module.Dual k (Y ⟶ ↑J)) (b : DirectSum (Fiber F X) fun (J : Fiber F X) => Z ⟶ ↑J) : ((directSumDualToDual fun (J : Fiber F X) => Z ⟶ ↑J) ((targetFiberDualMap F X f) a)) b = ((directSumDualToDual fun (J : Fiber F X) => Y ⟶ ↑J) a) ((targetFiberPrecomp F X f) b)

Componentwise dualized precomposition is adjoint to precomposition on the fixed-target Hom direct sum under the canonical direct-sum pairing.

noncomputable def MagnitudeConjecture.LinearCovering.targetFiberDualCorepresentablePullbackIso {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : IsCovering F) (X : D) (hfinite : ∀ (Y : C), {J : Fiber F X | Nontrivial (Y ⟶ ↑J)}.Finite) : targetFiberDualCorepresentableLinearModule F X ≅ linearModulePullback F (CoveringHom.dualLinearYonedaLinearModule X)

A covering identifies the fixed-target-fibre sum of dual corepresentables with the pullback of the downstairs dual corepresentable.