Radical morphisms in a finite deck-orbit category #
For locally finite objects with local endomorphism rings and a deck action free on isomorphism classes, a finite-support shift-orbit morphism is radical exactly when each of its homogeneous components is radical upstairs. This is the pointwise input for push-down of the projective radical boundary.
theorem
MagnitudeConjecture.CoveringHom.not_isZero_of_end_isLocalRing
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
[IsLocalRing (CategoryTheory.End X)]
:
¬CategoryTheory.Limits.IsZero X
A local endomorphism ring makes its object nonzero.
theorem
MagnitudeConjecture.CoveringHom.isIso_of_isSplitMono_to_localEnd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{X Y : C}
[IsLocalRing (CategoryTheory.End Y)]
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
(hX : ¬CategoryTheory.Limits.IsZero X)
:
CategoryTheory.IsIso f
A split monomorphism into an object with local endomorphism ring is an isomorphism as soon as its source is nonzero. Unlike the biproduct version, this uses only the local-ring idempotent dichotomy.
theorem
MagnitudeConjecture.CoveringHom.shiftOrbitOf_eq_zero_comp_objectShiftIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{A : Type w}
[AddGroup A]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
{X Y : C}
(a : A)
(f : ShiftHom X Y a)
:
(shiftOrbitOf X Y a) f = (shiftOrbitCompHom ((shiftOrbitOf X ((CategoryTheory.shiftFunctor C a).obj Y) 0) (shiftHomZero f)))
(ShiftOrbitCategory.objectShiftIso Y a).inv
A homogeneous orbit morphism is the degree-zero inclusion of its underlying map followed by the canonical isomorphism from the shifted target back to the target.
theorem
MagnitudeConjecture.CoveringHom.shiftOrbitOf_isSplitMono_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{A : Type w}
[AddGroup A]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
(k : Type uK)
[Field k]
[CategoryTheory.Linear k C]
{X Y : C}
(a : A)
(f : ShiftHom X Y a)
:
CategoryTheory.IsSplitMono
(have this := (shiftOrbitOf X Y a) f;
this) ↔ CategoryTheory.IsSplitMono f
Split-monicity of a homogeneous orbit morphism is equivalent to split-monicity of its upstairs component.
theorem
MagnitudeConjecture.CoveringHom.shiftOrbitOf_isRadicalMorphism_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{A : Type w}
[AddGroup A]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
(k : Type uK)
[Field k]
[CategoryTheory.Linear k C]
{X Y : C}
[IsLocalRing (CategoryTheory.End X)]
[IsLocalRing
(CategoryTheory.End
(have this := X;
this))]
(a : A)
(f : ShiftHom X Y a)
:
With local endomorphism rings on the upstairs source and the orbit source, a homogeneous orbit morphism is radical exactly when its component is radical upstairs.
theorem
MagnitudeConjecture.CoveringHom.eq_of_isIso_shiftHom_of_isIso_shiftHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type w}
[AddGroup A]
[CategoryTheory.HasShift C A]
{X Y : C}
{a b : A}
(htrivial : ∀ (c : A), Nonempty (Y ≅ (CategoryTheory.shiftFunctor C c).obj Y) → c = 0)
(f : ShiftHom X Y a)
(g : ShiftHom X Y b)
[CategoryTheory.IsIso f]
[CategoryTheory.IsIso g]
:
a = b
Triviality of the shift stabilizer makes the degree of an isomorphism between two translates unique.
theorem
MagnitudeConjecture.CoveringHom.shiftOrbitHom_isRadicalMorphism_iff_components
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{A : Type w}
[AddGroup A]
[CategoryTheory.HasShift C A]
[∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive]
(k : Type uK)
[Field k]
[CategoryTheory.Linear k C]
(hlocal : ∀ (Z : C), IsLocalRing (CategoryTheory.End Z))
(horbitLocal :
∀ (Z : C),
IsLocalRing
(CategoryTheory.End
(have this := Z;
this)))
(htrivial : ∀ (Y : C) (a : A), Nonempty (Y ≅ (CategoryTheory.shiftFunctor C a).obj Y) → a = 0)
(X Y : C)
(q : ShiftOrbitHom A X Y)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(have this := q;
this) ↔ ∀ (a : A), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (q a)
Under localness and a trivial target shift stabilizer, a shift-orbit morphism is radical exactly when all homogeneous components are radical.
noncomputable def
MagnitudeConjecture.CoveringHom.orbitPushdownRadicalToRepresentable
{kR : Type vR}
[Field kR]
{CR : Type uR}
[CategoryTheory.Category.{vR, uR} CR]
[CategoryTheory.Preadditive CR]
[CategoryTheory.Linear kR CR]
{AR : Type vR}
[AddGroup AR]
[CategoryTheory.HasShift CR AR]
[∀ (a : AR), (CategoryTheory.shiftFunctor CR a).Additive]
[∀ (a : AR), CategoryTheory.Functor.Linear kR (CategoryTheory.shiftFunctor CR a)]
(X : CR)
:
orbitPushdown (radicalLinearCoyoneda X) ⟶ (CategoryTheory.linearCoyoneda kR (ShiftOrbitCategory CR AR)).obj
(Opposite.op
(have this := X;
this))
The diagonal inclusion from the push-down of rad(X,-) into the
push-down of Hom(X,-), followed by the canonical orbit-representable
comparison.
Instances For
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownRadicalToRepresentable_app_apply
{kR : Type vR}
[Field kR]
{CR : Type uR}
[CategoryTheory.Category.{vR, uR} CR]
[CategoryTheory.Preadditive CR]
[CategoryTheory.Linear kR CR]
{AR : Type vR}
[AddGroup AR]
[CategoryTheory.HasShift CR AR]
[∀ (a : AR), (CategoryTheory.shiftFunctor CR a).Additive]
[∀ (a : AR), CategoryTheory.Functor.Linear kR (CategoryTheory.shiftFunctor CR a)]
(X Y : CR)
(z : orbitPushdownValue (radicalLinearCoyoneda X) Y)
:
(CategoryTheory.ConcreteCategory.hom ((orbitPushdownRadicalToRepresentable X).app Y)) z = (DirectSum.lmap fun (a : AR) =>
ModuleCat.Hom.hom ((radicalLinearCoyonedaInclusionNatTrans X).app ((CategoryTheory.shiftFunctor CR a).obj Y)))
z
Pointwise, the preceding comparison simply forgets each component's radical-membership proof.
noncomputable def
MagnitudeConjecture.CoveringHom.orbitPushdownRadicalLinearCoyonedaComparison
{kR : Type vR}
[Field kR]
{CR : Type uR}
[CategoryTheory.Category.{vR, uR} CR]
[CategoryTheory.Preadditive CR]
[CategoryTheory.Linear kR CR]
{AR : Type vR}
[AddGroup AR]
[CategoryTheory.HasShift CR AR]
[∀ (a : AR), (CategoryTheory.shiftFunctor CR a).Additive]
[∀ (a : AR), CategoryTheory.Functor.Linear kR (CategoryTheory.shiftFunctor CR a)]
(X : CR)
(hcomponents :
∀ (Y : CR) (q : ShiftOrbitHom AR X Y),
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(have this := q;
this) ↔ ∀ (a : AR), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (q a))
:
orbitPushdown (radicalLinearCoyoneda X) ⟶ radicalLinearCoyoneda
(have this := X;
this)
Before choosing orbit representatives, push-down of the radical representable maps canonically to the radical of the orbit representable.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.orbitPushdownRadicalLinearCoyonedaIso
{kR : Type vR}
[Field kR]
{CR : Type uR}
[CategoryTheory.Category.{vR, uR} CR]
[CategoryTheory.Preadditive CR]
[CategoryTheory.Linear kR CR]
{AR : Type vR}
[AddGroup AR]
[CategoryTheory.HasShift CR AR]
[∀ (a : AR), (CategoryTheory.shiftFunctor CR a).Additive]
[∀ (a : AR), CategoryTheory.Functor.Linear kR (CategoryTheory.shiftFunctor CR a)]
(X : CR)
(hcomponents :
∀ (Y : CR) (q : ShiftOrbitHom AR X Y),
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(have this := q;
this) ↔ ∀ (a : AR), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (q a))
:
orbitPushdown (radicalLinearCoyoneda X) ≅ radicalLinearCoyoneda
(have this := X;
this)
The raw orbit radical comparison is an isomorphism: its inverse regroups the finitely many homogeneous radical components.
Instances For
theorem
MagnitudeConjecture.CoveringHom.orbitPushdownRadicalLinearCoyonedaIso_hom_comp_inclusion
{kR : Type vR}
[Field kR]
{CR : Type uR}
[CategoryTheory.Category.{vR, uR} CR]
[CategoryTheory.Preadditive CR]
[CategoryTheory.Linear kR CR]
{AR : Type vR}
[AddGroup AR]
[CategoryTheory.HasShift CR AR]
[∀ (a : AR), (CategoryTheory.shiftFunctor CR a).Additive]
[∀ (a : AR), CategoryTheory.Functor.Linear kR (CategoryTheory.shiftFunctor CR a)]
(X : CR)
(hcomponents :
∀ (Y : CR) (q : ShiftOrbitHom AR X Y),
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(have this := q;
this) ↔ ∀ (a : AR), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (q a))
:
CategoryTheory.CategoryStruct.comp (orbitPushdownRadicalLinearCoyonedaIso X hcomponents).hom
(radicalLinearCoyonedaInclusionNatTrans
(have this := X;
this)) = CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans (radicalLinearCoyonedaInclusionNatTrans X))
(orbitPushdownLinearCoyonedaIso X).hom
The raw radical comparison is the restriction of the canonical projective-representable push-down comparison.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.object_trivialShiftStabilizer
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
{G : Type v'}
[Group G]
[MulAction G C']
(D : CoherentDeckShift C' G)
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
(a : Additive G)
:
Nonempty (X ≅ (CategoryTheory.shiftFunctor C' a).obj X) → a = 0
Freeness of the deck action on isomorphism classes gives a trivial stabilizer for every object under the associated additive shift.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbit_end_isLocalRing
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
IsLocalRing
(CategoryTheory.End
(have this := X;
this))
The shift-orbit endomorphism ring of every upstairs object is local. It is transported from the corresponding deck-orbit-skeleton vertex.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitHom_isRadicalMorphism_iff_components
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X Y : C')
(q : ShiftOrbitHom (Additive G) X Y)
:
QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism
(have this := q;
this) ↔ ∀ (a : Additive G), QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (q a)
Deck-specialized componentwise criterion for categorical radical morphisms in the shift-orbit category.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownRadicalLinearCoyonedaIso
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
orbitPushdown (radicalLinearCoyoneda X) ≅ radicalLinearCoyoneda
(have this := X;
this)
Before choosing orbit representatives, Gabriel push-down sends the radical of an upstairs projective representable to the radical of the corresponding shift-orbit representable.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownRadicalLinearCoyonedaIso_hom_comp_inclusion
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
CategoryTheory.CategoryStruct.comp (D.orbitPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom
(radicalLinearCoyonedaInclusionNatTrans
(have this := X;
this)) = CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans (radicalLinearCoyonedaInclusionNatTrans X))
(orbitPushdownLinearCoyonedaIso X).hom
The deck-specialized raw radical comparison is compatible with the projective-representable comparison.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeFunctor_map_isRadicalMorphism_iff
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
{X Y : MulAction.orbitRel.Quotient G C'}
(f :
(have this := X;
this) ⟶ have this := Y;
this)
:
Radicality agrees in the chosen orbit skeleton and in the ambient shift-orbit category.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeRadicalHomLinearEquiv
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X Y : MulAction.orbitRel.Quotient G C')
:
↥(CategoryTheory.radicalHomSubmodule k'
(have this := deckOrbitRepresentative X;
this)
(have this := deckOrbitRepresentative Y;
this)) ≃ₗ[k'] ↥(CategoryTheory.radicalHomSubmodule k'
(have this := X;
this)
(have this := Y;
this))
At chosen representatives, the ambient and induced-category radical Hom spaces are canonically linearly equivalent.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeRadicalLinearCoyonedaIso
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : MulAction.orbitRel.Quotient G C')
:
deckOrbitRepresentativeFunctor.comp
(radicalLinearCoyoneda
(have this := deckOrbitRepresentative X;
this)) ≅ radicalLinearCoyoneda
(have this := X;
this)
Restricting the radical representable at a chosen representative gives the literal radical representable on the deck-orbit skeleton.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeRadicalLinearCoyonedaIso_hom_comp_inclusion
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : MulAction.orbitRel.Quotient G C')
:
CategoryTheory.CategoryStruct.comp (D.deckOrbitRepresentativeRadicalLinearCoyonedaIso hP hlocal hfree X).hom
(radicalLinearCoyonedaInclusionNatTrans
(have this := X;
this)) = CategoryTheory.CategoryStruct.comp
(deckOrbitRepresentativeFunctor.whiskerLeft
(radicalLinearCoyonedaInclusionNatTrans
(have this := deckOrbitRepresentative X;
this)))
(deckOrbitRepresentativeLinearCoyonedaIso X).hom
The chosen-representative radical comparison is the restriction of the corresponding representable comparison.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownRadicalLinearCoyonedaIso
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
orbitSkeletonPushdown (radicalLinearCoyoneda X) ≅ radicalLinearCoyoneda (Quotient.mk'' X)
Skeletal Gabriel push-down sends the radical of the projective
representable at X to the radical of the projective representable at the
strict orbit of X.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownRadicalLinearCoyonedaIso_hom_comp_inclusion
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
CategoryTheory.CategoryStruct.comp (D.orbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom
(radicalLinearCoyonedaInclusionNatTrans (Quotient.mk'' X)) = CategoryTheory.CategoryStruct.comp
(deckOrbitRepresentativeFunctor.whiskerLeft (orbitPushdownNatTrans (radicalLinearCoyonedaInclusionNatTrans X)))
(D.orbitSkeletonPushdownLinearCoyonedaIso X).hom
The skeletal radical comparison and projective-representable comparison identify the pushed radical inclusion with the literal downstairs radical inclusion.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
linearModuleOrbitSkeletonPushdown.obj (radicalLinearCoyonedaLinearModule X) ≅ radicalLinearCoyonedaLinearModule (Quotient.mk'' X)
Bundled linear-module form of skeletal push-down preserving the radical of a projective representable.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso_hom_hom
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
(D.linearModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom.hom = (D.orbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalLinearCoyonedaRadical
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(X : C')
:
The finite downstairs radical projective associated to the strict orbit
of X.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
Finite-dimensional skeletal push-down preserves the radical of a finite projective representable.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso_hom_hom
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
(D.finiteDimensionalModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom.hom = (D.linearModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownRadicalInclusion
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
have hP' := ⋯;
CategoryTheory.CategoryStruct.comp
(D.finiteDimensionalModuleOrbitSkeletonPushdownRadicalLinearCoyonedaIso hP hlocal hfree X).hom
(finiteDimensionalLinearCoyonedaRadicalInclusion (Quotient.mk'' X) ⋯) = CategoryTheory.CategoryStruct.comp
(D.finiteDimensionalModuleOrbitSkeletonPushdown.map (finiteDimensionalLinearCoyonedaRadicalInclusion X ⋯))
(D.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaIso X ⋯).hom
Finite-dimensional push-down carries the literal radical inclusion of an upstairs projective representable to the literal radical inclusion of the corresponding downstairs projective representable.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownRadicalInclusion_isRightAlmostSplit
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
:
Finite-dimensional skeletal push-down sends the radical inclusion of a projective representable to a right almost-split morphism.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.exists_pushedIndecomposable_of_irreducible_to_projectivePushdown
{k' : Type v'}
[Field k']
{C' : Type u'}
[CategoryTheory.Category.{v', u'} C']
[CategoryTheory.Preadditive C']
{G : Type v'}
[Group G]
[MulAction G C']
[IsCancelSMul G C']
[CategoryTheory.Linear k' C']
(D : CoherentDeckShift C' G)
[∀ (a : Additive G), (D.core.F a).Additive]
[∀ (a : Additive G), CategoryTheory.Functor.Linear k' (D.core.F a)]
[IsMulTorsionFree G]
(hP : ∀ (X : C'), IsFiniteDimensionalModule k' (linearCoyonedaLinearModule X))
(hlocal : ∀ (X : C'), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(X : C')
{Y : FiniteDimensionalModuleCategory k'}
(hY : CategoryTheory.Indecomposable Y)
(f : Y ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj (finiteDimensionalLinearCoyoneda X ⋯))
(hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f)
:
∃ (Z : FiniteDimensionalModuleCategory k'),
CategoryTheory.Indecomposable Z ∧ Nonempty (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj Z ≅ Y)
Projective boundary adjacency: every indecomposable with an irreducible map to the push-down of an upstairs projective representable is itself the push-down of an upstairs indecomposable.