Essential surjectivity of the primitive restricted Yoneda functor #
Iyama saturation enlarges the lifted image of a represented boundary cover inside a full-generator representable. The strict-tau homological estimates make that saturated image projective, so the additive Auslander equivalence returns it to a literal factor object.
The boundary idempotent shows that the boundary cover remains surjective after this replacement. Its weak-cokernel property then identifies the represented factor object with the original poset-space subobject. Consequently the restricted Yoneda image is closed under subobjects and, using the full-support envelope, essentially surjective.
theorem
MagnitudeConjecture.PosetSpace.BoundarySurjective.of_comp
{k T : Type u}
[Field k]
[PartialOrder T]
{X Y Z : Obj k T}
{f : X ⟶ Y}
{g : Y ⟶ Z}
(hf : BoundarySurjective f)
(hfg : BoundarySurjective (CategoryTheory.CategoryStruct.comp f g))
:
theorem
MagnitudeConjecture.PosetSpace.linear_injective_of_mono
{k T : Type u}
[Field k]
[PartialOrder T]
{X Y : Obj k T}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Function.Injective ⇑f.linear
noncomputable def
MagnitudeConjecture.PosetSpace.isoOfBoundarySurjectiveOfInjective
{k T : Type u}
[Field k]
[PartialOrder T]
{X Y : Obj k T}
(f : X ⟶ Y)
(hboundary : BoundarySurjective f)
(hinjective : Function.Injective ⇑f.linear)
:
X ≅ Y
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_factorObject_representing_saturatedSubobjectImage_unconditional
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
∃ (Z : S.FactorCategory K),
Nonempty
((CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).obj Z ≅ ModuleCat.of (S.factorAuslanderRing K) ↥(R.saturatedSubobjectImage H m))
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedFactorObject
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
S.FactorCategory K
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedFactorObjectIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
(CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).obj (R.saturatedFactorObject H m) ≅ ModuleCat.of (S.factorAuslanderRing K) ↥(R.saturatedSubobjectImage H m)
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedSubobjectAuslanderToSaturation
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
(S.factorAdditiveGenerator K ⟶ R.boundaryCoverObject Y) →ₗ[S.factorAuslanderRing K] ↥(R.saturatedSubobjectImage H m)
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedBoundaryCoverFactor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
R.boundaryCoverObject Y ⟶ R.saturatedFactorObject H m
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.map_saturatedBoundaryCoverFactor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
(CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).map (R.saturatedBoundaryCoverFactor H m) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (R.liftedSubobjectAuslanderToSaturation H m))
(R.saturatedFactorObjectIso H m).inv
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedFactorInclusion
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
R.saturatedFactorObject H m ⟶ X
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.map_saturatedFactorInclusion
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
(CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).map (R.saturatedFactorInclusion H m) = CategoryTheory.CategoryStruct.comp (R.saturatedFactorObjectIso H m).hom
(ModuleCat.ofHom (R.saturatedSubobjectImage H m).subtype)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedBoundaryCoverFactor_comp_inclusion
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.CategoryStruct.comp (R.saturatedBoundaryCoverFactor H m) (R.saturatedFactorInclusion H m) = R.liftedSubobjectCoverMap H m
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedFactorInclusion_mono
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.Mono (R.saturatedFactorInclusion H m)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedBoundaryCoverFactor_postcomposition_surjective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
Function.Surjective fun (a : S.factorProjectiveGenerator K ⟶ R.boundaryCoverObject Y) =>
CategoryTheory.CategoryStruct.comp a (R.saturatedBoundaryCoverFactor H m)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representableData_map_boundarySurjective_of_projectiveGenerator
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
{B Z : S.FactorCategory K}
(p : B ⟶ Z)
(hp : Function.Surjective fun (a : S.factorProjectiveGenerator K ⟶ B) => CategoryTheory.CategoryStruct.comp a p)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedBoundaryCoverFactor_boundarySurjective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedBoundaryRelationMap_comp_saturatedBoundaryCoverFactor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.CategoryStruct.comp (R.liftedBoundaryRelationMap H Y) (R.saturatedBoundaryCoverFactor H m) = 0
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.map_liftedBoundaryRelationMap_comp_saturatedBoundaryCoverFactor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.CategoryStruct.comp (R.representableData.map (R.liftedBoundaryRelationMap H Y))
(R.representableData.map (R.saturatedBoundaryCoverFactor H m)) = 0
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedRealizationMap
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
Y ⟶ R.representableData.obj (R.saturatedFactorObject H m)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryCoverMap_comp_saturatedRealizationMap
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.CategoryStruct.comp (R.representedBoundaryCoverMap H Y) (R.saturatedRealizationMap H m) = R.representableData.map (R.saturatedBoundaryCoverFactor H m)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedRealizationMap_boundarySurjective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedRealizationMap_comp_inclusion
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
:
CategoryTheory.CategoryStruct.comp (R.saturatedRealizationMap H m)
(R.representableData.map (R.saturatedFactorInclusion H m)) = m
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedRealizationIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
{Y : PosetSpace.Obj k T}
{X : S.FactorCategory K}
(m : Y ⟶ R.representableData.obj X)
[CategoryTheory.Mono m]
:
Y ≅ R.representableData.obj (R.saturatedFactorObject H m)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representable_closedUnderSubobjects
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representable_essentiallySurjective
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(hsink : D.multiplicity ↑D.sink = 1)
(Y : PosetSpace.Obj k T)
:
∃ (X : S.FactorCategory K), Nonempty (R.representableData.obj X ≅ Y)