Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleOrdinaryQuiverFullness

Fullness for arbitrary ordinary-arrow representatives #

Any representatives of the ordinary arrows span the first layer of the radical filtration. Their composites then span every successive layer modulo the next one, and nilpotence terminates the approximation. Over an algebraically closed field, an endomorphism of an indecomposable projective is a scalar identity modulo the radical, so every representative-dependent free path realization is full.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fullnessRestrictedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (i : Fin S.n) :
Module k ↑(S.almostSplitSkeleton.obj i)
Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fullnessRestrictedScalarTower {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (i : Fin S.n) :
    IsScalarTower k Aᵐᵒᵖ ↑(S.almostSplitSkeleton.obj i)
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x y : S.ProjectiveLabel) :
    Submodule k (S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x)

    The realized linear combinations of ordinary paths from x to y.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hom_mem_pathImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (a : S.OrdinaryArrow x y) :
      D.hom a ∈ D.pathImage x y
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.identity_mem_pathImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x : S.ProjectiveLabel) :
      CategoryTheory.CategoryStruct.id (S.ordinaryProjectiveObj x) ∈ D.pathImage x x
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathImage_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y z : S.ProjectiveLabel} {f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj z} {g : S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj x} (hf : f ∈ D.pathImage z y) (hg : g ∈ D.pathImage x z) :
      CategoryTheory.CategoryStruct.comp f g ∈ D.pathImage x y

      Realized path combinations are closed under composition.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_pathImage_radical_approximation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} {f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x} (hf : f ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)) :
      ∃ g ∈ D.pathImage x y, g ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x) ∧ f - g ∈ (S.projectiveNilpotentRadicalData.ideal.pow 2).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

      A radical morphism is a realized linear combination of arrows modulo the square of the projective radical.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_pathImage_radicalPower_approximation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (n : ℕ) {x y : S.ProjectiveLabel} {f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x} :
      f ∈ (S.projectiveNilpotentRadicalData.ideal.pow (n + 1)).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x) → ∃ g ∈ D.pathImage x y, g ∈ (S.projectiveNilpotentRadicalData.ideal.pow (n + 1)).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x) ∧ f - g ∈ (S.projectiveNilpotentRadicalData.ideal.pow (n + 2)).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

      Every positive projective-radical layer is represented by realized paths modulo the next layer. The representative remains in the original layer.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.radicalPower_mem_pathImage_of_pow_add_eq_bot {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (r n : ℕ) {x y : S.ProjectiveLabel} {f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x} :
      1 ≤ n → S.projectiveNilpotentRadicalData.ideal.pow (n + r) = ⊥ → f ∈ (S.projectiveNilpotentRadicalData.ideal.pow n).hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x) → f ∈ D.pathImage x y

      If a later radical layer vanishes, every morphism in a positive earlier layer is already a realized linear combination of paths.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.projectiveRadical_le_ordinaryPathImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (x y : S.ProjectiveLabel) :
      S.projectiveNilpotentRadicalData.ideal.homSubmodule (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x) ≤ D.pathImage x y

      Every projective-radical morphism is a realized linear combination of ordinary paths.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_projectiveRadical_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (hxy : x ≠ y) (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) :
      f ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj y) (S.ordinaryProjectiveObj x)

      A morphism between differently labelled selected projectives belongs to the projective radical.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_scalar_sub_mem_projectiveRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) (x : S.ProjectiveLabel) (f : S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj x) :
      ∃ (a : k), f - a • CategoryTheory.CategoryStruct.id (S.ordinaryProjectiveObj x) ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj x) (S.ordinaryProjectiveObj x)

      An endomorphism of a selected indecomposable projective is a scalar identity modulo the projective radical.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.pathImage_eq_top {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) (x y : S.ProjectiveLabel) :
      D.pathImage x y = ⊤

      Paths realized by any representative system span every morphism between selected indecomposable projectives.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_realization_preimage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) {x y : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) :
      ∃ (q : LinearPathCategory.obj k S.ProjectiveLabel y ⟶ LinearPathCategory.obj k S.ProjectiveLabel x), D.realization.map q = f

      Every morphism between selected projectives has a preimage in the free linear path category under any representative realization.

      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.realization_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (D : OrdinaryArrowRepresentatives) :
      D.realization.Full

      Every free linear ordinary-quiver realization is full.