Linear covering functors #
This file records the direct-sum Hom-space definition of a covering functor. For a fixed lift of either endpoint, mapping morphisms and summing over all lifts of the other endpoint must give a bijection onto the Hom space downstairs. This is the categorical covering notion used in the Bongartz--Gabriel argument; surjectivity on objects is kept as a separate property.
theorem
MagnitudeConjecture.LinearCovering.bijective_of_surjective_quotient_square
{k : Type u}
[Field k]
{A : Type u_1}
{A' : Type u_2}
{B : Type u_3}
{B' : Type u_4}
[AddCommGroup A]
[AddCommGroup A']
[AddCommGroup B]
[AddCommGroup B']
[Module k A]
[Module k A']
[Module k B]
[Module k B']
(e : A ≃ₗ[k] B)
(qA : A →ₗ[k] A')
(qB : B →ₗ[k] B')
(g : A' →ₗ[k] B')
(hqA : Function.Surjective ⇑qA)
(hqB : Function.Surjective ⇑qB)
(hsquare : ∀ (a : A), g (qA a) = qB (e a))
(hker : ∀ (a : A), qB (e a) = 0 → qA a = 0)
:
Function.Bijective ⇑g
A bijective linear map remains bijective after passing through a surjective quotient square, provided that every element which becomes zero downstairs already becomes zero in the source quotient. This is the linear algebra core used to descend covering-functor Hom equivalences through relation ideals.
@[reducible, inline]
abbrev
MagnitudeConjecture.LinearCovering.Fiber
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
(F : CategoryTheory.Functor C D)
(Y : D)
:
Type v₁
The objects upstairs mapping literally to a chosen target object.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.targetFiberHomMap
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(X : C)
(Y : D)
:
Map the summand with fixed source X and varying lifted target into the
corresponding Hom space downstairs.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.sourceFiberHomMap
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(X : D)
(Y : C)
:
Map the summand with fixed target Y and varying lifted source into the
corresponding Hom space downstairs.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.targetFiberLof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : C)
(Y : D)
(Z : Fiber F Y)
:
Inclusion of one fixed-source lifted Hom space into the target-fibre direct sum.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.sourceFiberLof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : D)
(Y : C)
(Z : Fiber F X)
:
Inclusion of one fixed-target lifted Hom space into the source-fibre direct sum.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.targetFiberPrecomp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(Y : D)
{X' X : C}
(e : X' ⟶ X)
:
Precompose every fixed-target-fibre summand by one morphism upstairs.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.sourceFiberPostcomp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : D)
{Y Z : C}
(e : Y ⟶ Z)
:
Postcompose every fixed-source-fibre summand by one morphism upstairs.
Instances For
@[simp]
theorem
MagnitudeConjecture.LinearCovering.targetFiberHomMap_lof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(X : C)
(Y : D)
(Z : Fiber F Y)
(f : X ⟶ ↑Z)
:
(targetFiberHomMap F X Y) ((targetFiberLof F X Y Z) f) = CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.eqToHom ⋯)
@[simp]
theorem
MagnitudeConjecture.LinearCovering.sourceFiberHomMap_lof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(X : D)
(Y : C)
(Z : Fiber F X)
(f : ↑Z ⟶ Y)
:
(sourceFiberHomMap F X Y) ((sourceFiberLof F X Y Z) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (F.map f)
@[simp]
theorem
MagnitudeConjecture.LinearCovering.targetFiberPrecomp_lof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(Y : D)
{X' X : C}
(e : X' ⟶ X)
(W : Fiber F Y)
(f : X ⟶ ↑W)
:
(targetFiberPrecomp F Y e) ((targetFiberLof F X Y W) f) = (targetFiberLof F X' Y W) (CategoryTheory.CategoryStruct.comp e f)
@[simp]
theorem
MagnitudeConjecture.LinearCovering.targetFiberPrecomp_apply
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(Y : D)
{X' X : C}
(e : X' ⟶ X)
(a : DirectSum (Fiber F Y) fun (W : Fiber F Y) => X ⟶ ↑W)
(V : Fiber F Y)
:
((targetFiberPrecomp F Y e) a) V = CategoryTheory.CategoryStruct.comp e (a V)
Precomposition in a target fibre acts componentwise.
@[simp]
theorem
MagnitudeConjecture.LinearCovering.sourceFiberPostcomp_lof
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : D)
{Y Z : C}
(e : Y ⟶ Z)
(W : Fiber F X)
(f : ↑W ⟶ Y)
:
(sourceFiberPostcomp F X e) ((sourceFiberLof F X Y W) f) = (sourceFiberLof F X Z W) (CategoryTheory.CategoryStruct.comp f e)
@[simp]
theorem
MagnitudeConjecture.LinearCovering.sourceFiberPostcomp_apply
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : D)
{Y Z : C}
(e : Y ⟶ Z)
(a : DirectSum (Fiber F X) fun (W : Fiber F X) => ↑W ⟶ Y)
(V : Fiber F X)
:
((sourceFiberPostcomp F X e) a) V = CategoryTheory.CategoryStruct.comp (a V) e
Postcomposition in a source fibre acts componentwise.
theorem
MagnitudeConjecture.LinearCovering.targetFiberHomMap_targetFiberPrecomp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(Y : D)
{X' X : C}
(e : X' ⟶ X)
(a : DirectSum (Fiber F Y) fun (W : Fiber F Y) => X ⟶ ↑W)
:
(targetFiberHomMap F X' Y) ((targetFiberPrecomp F Y e) a) = CategoryTheory.CategoryStruct.comp (F.map e) ((targetFiberHomMap F X Y) a)
The fixed-source fibre map intertwines precomposition upstairs with precomposition by the mapped morphism downstairs.
theorem
MagnitudeConjecture.LinearCovering.sourceFiberHomMap_sourceFiberPostcomp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
(X : D)
{Y Z : C}
(e : Y ⟶ Z)
(a : DirectSum (Fiber F X) fun (W : Fiber F X) => ↑W ⟶ Y)
:
(sourceFiberHomMap F X Z) ((sourceFiberPostcomp F X e) a) = CategoryTheory.CategoryStruct.comp ((sourceFiberHomMap F X Y) a) (F.map e)
The fixed-target fibre map intertwines postcomposition upstairs with postcomposition by the mapped morphism downstairs.
theorem
MagnitudeConjecture.LinearCovering.sourceFiberPostcomp_comp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(X : D)
{Y Z W : C}
(e : Y ⟶ Z)
(f : Z ⟶ W)
(a : DirectSum (Fiber F X) fun (V : Fiber F X) => ↑V ⟶ Y)
:
(sourceFiberPostcomp F X f) ((sourceFiberPostcomp F X e) a) = (sourceFiberPostcomp F X (CategoryTheory.CategoryStruct.comp e f)) a
Successive postcomposition of a source-fibre family is postcomposition by the composite upstairs.
theorem
MagnitudeConjecture.LinearCovering.targetFiberPrecomp_comp
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Linear k C]
(F : CategoryTheory.Functor C D)
(Y : D)
{X'' X' X : C}
(e : X'' ⟶ X')
(f : X' ⟶ X)
(a : DirectSum (Fiber F Y) fun (V : Fiber F Y) => X ⟶ ↑V)
:
(targetFiberPrecomp F Y e) ((targetFiberPrecomp F Y f) a) = (targetFiberPrecomp F Y (CategoryTheory.CategoryStruct.comp e f)) a
Successive precomposition of a target-fibre family is precomposition by the composite upstairs.
structure
MagnitudeConjecture.LinearCovering.IsCovering
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k C]
[CategoryTheory.Linear k D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
:
A linear covering functor: after fixing either lifted endpoint, the Hom space downstairs is the direct sum of the Hom spaces over all lifts of the other endpoint.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.IsCovering.targetFiberHomLinearEquiv
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
:
The fixed-source direct-sum Hom equivalence supplied by a covering functor.
Instances For
noncomputable def
MagnitudeConjecture.LinearCovering.IsCovering.sourceFiberHomLinearEquiv
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
:
The fixed-target direct-sum Hom equivalence supplied by a covering functor.
Instances For
@[simp]
theorem
MagnitudeConjecture.LinearCovering.IsCovering.targetFiberHomLinearEquiv_apply
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
(f : DirectSum (Fiber F Y) fun (Z : Fiber F Y) => X ⟶ ↑Z)
:
(hF.targetFiberHomLinearEquiv X Y) f = (targetFiberHomMap F X Y) f
@[simp]
theorem
MagnitudeConjecture.LinearCovering.IsCovering.sourceFiberHomLinearEquiv_apply
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
(f : DirectSum (Fiber F X) fun (Z : Fiber F X) => ↑Z ⟶ Y)
:
(hF.sourceFiberHomLinearEquiv X Y) f = (sourceFiberHomMap F X Y) f
theorem
MagnitudeConjecture.LinearCovering.IsCovering.map_injective
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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 Y : C)
:
Function.Injective F.map
Every linear covering functor is faithful: an individual Hom space is one summand of either covering decomposition.
theorem
MagnitudeConjecture.LinearCovering.IsCovering.faithful
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
:
F.Faithful
The faithful structure carried by a linear covering functor.
theorem
MagnitudeConjecture.LinearCovering.IsCovering.map_bijective_of_obj_injective
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
(hobj : Function.Injective F.obj)
(X Y : C)
:
Function.Bijective F.map
A covering functor which is injective on objects is fully faithful.
Indeed, the fibre over F.obj Y then consists only of Y, so the
fixed-source covering isomorphism is just the ordinary map on the Hom space
X ⟶ Y.
noncomputable def
MagnitudeConjecture.LinearCovering.IsCovering.fullyFaithfulOfObjInjective
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
(hobj : Function.Injective F.obj)
:
F.FullyFaithful
A covering functor which is injective on objects, packaged as a fully faithful functor.
Instances For
theorem
MagnitudeConjecture.LinearCovering.IsCovering.isEquivalenceOfObjBijective
{k : Type u}
[Field k]
{C : Type v₁}
[CategoryTheory.Category.{w₁, v₁} C]
[CategoryTheory.Preadditive C]
{D : Type v₂}
[CategoryTheory.Category.{w₂, v₂} D]
[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)
(hobj : Function.Bijective F.obj)
:
F.IsEquivalence
A covering functor which is bijective on objects is an equivalence of categories.