The boundary idempotent and Iyama saturation

The boundary projective generator U is a retract of the full surviving additive generator G. Its projector defines an idempotent e in the factor Auslander ring (End G)ᵐᵒᵖ, and the represented module Hom(G,U) is the principal left ideal Γ e.

Together with IdempotentSaturation, this translates Iyama's condition HomΓ(Hom(G,U), M/L) = 0 into the explicit condition that e annihilates the quotient. The next layer will apply this saturation to the lifted image inside the represented full-support projective.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRing {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)) : Type u

The factor Auslander ring attached to the full surviving additive generator.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAdditiveGeneratorEnd_moduleFinite {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)) : Module.Finite k (CategoryTheory.End (S.factorAdditiveGenerator K))

The endomorphism algebra of the finite factor generator is finite over the coefficient field.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRing_isNoetherian {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)) : IsNoetherianRing (S.factorAuslanderRing K)

Hence the factor Auslander ring is Noetherian.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRepresentable_finiteProjective {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)) (X : S.FactorCategory K) : CategoryTheory.finiteProjectiveModules (S.factorAuslanderRing K) ((CategoryTheory.preadditiveCoyonedaObj (S.factorAdditiveGenerator K)).obj X)

Every full-generator representable is a finitely generated projective module over the factor Auslander ring.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderRepresentable_moduleFinite {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)) (X : S.FactorCategory K) : Module.Finite (S.factorAuslanderRing K) (S.factorAdditiveGenerator K ⟶ X)

Full-generator representables are finite modules.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryRepresentableFGObj {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)) : FGModuleCat (S.factorAuslanderRing K)

The represented boundary generator, bundled in the finitely generated module category of the factor Auslander algebra.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryRepresentableFGObj_projective {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)) : CategoryTheory.Projective (S.factorBoundaryRepresentableFGObj K)

The represented boundary generator is projective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryIdempotent {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)) : S.factorAuslanderRing K

The boundary projector, viewed as an idempotent in the factor Auslander ring.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorBoundaryIdempotent_isIdempotentElem {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)) : IsIdempotentElem (S.factorBoundaryIdempotent K)

The boundary projector is idempotent.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRepresentableToLeftIdeal {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)) (q : S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K) : ↥(IdempotentSaturation.principalLeftIdeal (S.factorBoundaryIdempotent K))

Embed the represented boundary projective in the regular Auslander module by postcomposing with the retract inclusion.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRepresentableFromLeftIdeal {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)) (y : ↥(IdempotentSaturation.principalLeftIdeal (S.factorBoundaryIdempotent K))) : S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K

Recover a boundary morphism from its principal-left-ideal coordinate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRepresentableLinearEquiv {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)) : (S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K) ≃ₗ[S.factorAuslanderRing K] ↥(IdempotentSaturation.principalLeftIdeal (S.factorBoundaryIdempotent K))

Under the full-generator representable functor, the boundary projective generator is the principal left ideal cut out by the boundary idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjectiveRepresentable_hom_eq_zero_iff {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)) {N : Type u} [AddCommGroup N] [Module (S.factorAuslanderRing K) N] : (∀ (f : (S.factorAdditiveGenerator K ⟶ S.factorProjectiveGenerator K) →ₗ[S.factorAuslanderRing K] N), f = 0) ↔ ∀ (x : N), S.factorBoundaryIdempotent K • x = 0

Iyama's vanishing condition for the boundary projective is exactly annihilation by the boundary idempotent.