The saturated Auslander image of a represented subobject #
Given a monomorphism from a poset space Y into a represented object, cover
Y by a represented boundary object and lift the composite into the factor
category. Full-generator restricted Yoneda sends the lift to a map between
projective modules. Its image L is enlarged by the boundary-idempotent
saturation constructed in RightModuleIyamaSaturation.
This is the literal module M in Iyama's proof of closure under subobjects.
The remaining homological layer proves that it is projective.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedSubobjectCoverMap
{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)
:
R.boundaryCoverObject Y ⟶ X
Lift the composite of the represented boundary cover with a map into a represented object.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.map_liftedSubobjectCoverMap
{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)
:
R.representableData.map (R.liftedSubobjectCoverMap H m) = CategoryTheory.CategoryStruct.comp (R.representedBoundaryCoverMap H Y) m
Restricted Yoneda sends the lifted cover to the requested composite.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedSubobjectAuslanderMap
{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] S.factorAdditiveGenerator K ⟶ X
The full-generator Auslander map induced by the lifted boundary cover.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedSubobjectImage
{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)
:
Submodule (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ X)
The raw image L of the lifted cover inside the represented Auslander
projective.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectImage
{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)
:
Submodule (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ X)
Iyama's module M: the maximal boundary-invisible enlargement of the
lifted image L.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.liftedSubobjectImage_le_saturatedSubobjectImage
{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)
:
R.liftedSubobjectImage H m ≤ R.saturatedSubobjectImage H m
The raw lifted image is contained in its saturation.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIdempotent_smul_mkQ_eq_zero_of_mem_saturatedSubobjectImage
{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)
{x : S.factorAdditiveGenerator K ⟶ X}
(hx : x ∈ R.saturatedSubobjectImage H m)
:
S.factorBoundaryIdempotent K • (R.liftedSubobjectImage H m).mkQ x = 0
The image of the saturation in the quotient by L is annihilated by
the boundary idempotent.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.le_saturatedSubobjectImage_of_boundaryIdempotent_smul_mkQ_eq_zero
{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)
(N : Submodule (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ X))
(hN : ∀ x ∈ N, S.factorBoundaryIdempotent K • (R.liftedSubobjectImage H m).mkQ x = 0)
:
N ≤ R.saturatedSubobjectImage H m
Maximality of the actual saturated image among enlargements of L that
are invisible to the boundary idempotent.
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectQuotientCoordinate
{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)
:
Submodule (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.liftedSubobjectImage H m)
The quotient coordinate M/L, realized as the full idempotent-torsion
submodule of the ambient quotient.
Instances For
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectAmbientQuotientFGObj
{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)
:
FGModuleCat (S.factorAuslanderRing K)
The quotient by Iyama's saturated image, bundled as a finitely generated module over the factor Auslander algebra.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.torsionSubmodule_saturatedSubobjectAmbientQuotient_eq_bot
{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)
:
Saturation removes all remaining boundary-idempotent torsion from the
ambient quotient P/M.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.submodule_eq_bot_of_hom_from_boundary_eq_zero
{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)
(N : Submodule (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m))
(hzero : ∀ (f : (S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K) →ₗ[S.factorAuslanderRing K] ↥N), f = 0)
:
N = ⊥
Every submodule of P/M invisible to the represented boundary
generator is zero. This is the essentiality consequence of Iyama's maximal
saturation, stated without choosing an injective hull.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectAmbientQuotientNakayamaMap
{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)
:
↑(R.saturatedSubobjectAmbientQuotientFGObj H m) →ₗ[S.factorAuslanderRing K] Fin (Module.finrank k (S.factorBoundaryRepresentableFGObj K ⟶ R.saturatedSubobjectAmbientQuotientFGObj H m)) →
↑(projectiveNakayamaFGObj (S.factorBoundaryRepresentableFGObj K))
The finite Nakayama evaluation map from the saturated ambient quotient to copies of the boundary Nakayama injective.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectAmbientQuotientNakayamaMap_injective
{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)
:
Function.Injective ⇑(R.saturatedSubobjectAmbientQuotientNakayamaMap H m)
Maximal saturation makes the finite boundary Nakayama evaluation map injective.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.hom_to_saturatedSubobjectQuotientCoordinate_eq_zero
{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)
(f :
(S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K) →ₗ[S.factorAuslanderRing K] ↥(R.saturatedSubobjectQuotientCoordinate H m))
:
f = 0
Iyama's boundary-Hom coordinate vanishes on M/L.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectQuotient_projectiveDimensionLE_one_of_injective
{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)
{I : Type u}
[AddCommGroup I]
[Module (S.factorAuslanderRing K) I]
(i : (S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m →ₗ[S.factorAuslanderRing K] I)
(hi : Function.Injective ⇑i)
(hI : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) I) 1)
(hcokernel : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) (I ⧸ i.range)) 2)
:
CategoryTheory.HasProjectiveDimensionLE
(ModuleCat.of (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m)) 1
The final dimension shift in Iyama's proof, separated from the two
strict-tau inputs that construct the injective hull and control the global
dimension. An embedding of P/M into a module of projective dimension at
most one has source of projective dimension at most one as soon as its
cokernel has projective dimension at most two.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectImage_projective_of_quotient_projectiveDimensionLE_one
{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)
(hquotient :
CategoryTheory.HasProjectiveDimensionLE
(ModuleCat.of (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m)) 1)
:
CategoryTheory.Projective (ModuleCat.of (S.factorAuslanderRing K) ↥(R.saturatedSubobjectImage H m))
The saturated image is projective once the source's remaining quotient projective-dimension bound is supplied.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_factorObject_representing_saturatedSubobjectImage
{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)
(hquotient :
CategoryTheory.HasProjectiveDimensionLE
(ModuleCat.of (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m)) 1)
:
∃ (Z : S.FactorCategory K),
Nonempty
((CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).obj Z ≅ ModuleCat.of (S.factorAuslanderRing K) ↥(R.saturatedSubobjectImage H m))
Once the quotient has projective dimension at most one, the saturated module returns to a literal object of the factor category under the full Auslander equivalence.