The local fullness step for a displayed right mesh

Ringel's standardness recursion chooses all arrows ending at one vertex as the occurrence components of a right almost-split sink. This file proves the two local facts needed by that recursion: those components reassemble to the supplied sink, and fullness at all strict predecessors extends to the current target.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instQuiverFinN_1 {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFintypeHomFinN_1 {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) : Fintype (i ⟶ j)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshNonprojectiveVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : { z : Fin S.n // z ∉ (S.rightMeshData H).projective }

A nonprojective module label as a nonprojective vertex of the concrete right mesh data.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshNonprojectiveVertex_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : ↑(S.rightMeshNonprojectiveVertex H z) = ↑z

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshData_tau_rightMeshNonprojectiveVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (S.rightMeshData H).tau (S.rightMeshNonprojectiveVertex H z) = S.rightTranslationLabel z

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshSinkArrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) {y : Fin S.n} (a : S.MeshArrow z y) : S.almostSplitSkeleton.obj y ⟶ S.almostSplitSkeleton.obj z

The arrow representative at one fixed target obtained by taking an occurrence component of a supplied map out of the displayed middle.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceArrowMapAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) {i j : Fin S.n} (a : S.MeshArrow i j) : S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i

Replace all arrow representatives ending at one fixed target by the occurrence components of g, leaving every other target unchanged.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceArrowMapAt_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) {y : Fin S.n} (a : S.MeshArrow z y) : S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g a = S.meshSinkArrowMap z g a

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.replaceArrowMapAt_eq_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) {i j : Fin S.n} (hiz : i ≠ z) (a : S.MeshArrow i j) : S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g a = arrowMap a

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.realizedRightMeshSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z

Assemble all representatives ending at z into a map out of its displayed middle.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.realizedRightMeshSink_replaceArrowMapAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) : S.realizedRightMeshSink (fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g) z = g

Taking all occurrence components and reassembling them recovers the original map out of the displayed middle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.realizedRightMeshSink_replaceArrowMapAt_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) (w : Fin S.n) (hwz : w ≠ z) : S.realizedRightMeshSink (fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g) w = S.realizedRightMeshSink (fun {i j : Fin S.n} => arrowMap) w

Updating the representatives ending at z leaves the assembled sink at every other target unchanged.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshProjectiveSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z

The radical inclusion transported from the literal projective radical to the uniform displayed middle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshProjectiveSink_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : CategoryTheory.Mono (S.meshProjectiveSink z hz)

The transported projective radical inclusion is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshProjectiveSink_rightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.meshProjectiveSink z hz)

The transported projective radical inclusion is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.lift_map_replaceArrowMapAt_eq_of_lt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) {x y : Fin S.n} (hyz : y < z) (p : LinearPathCategory.obj k (Fin S.n) x ⟶ LinearPathCategory.obj k (Fin S.n) y) : (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g).map p = (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map p

Changing representatives at a later target does not change free-path evaluation into an earlier target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshSourceMap_replaceArrowMapAt_eq_of_le {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : Fin S.n) (g : (S.meshRightAlmostSplitAt z).middle ⟶ S.almostSplitSkeleton.obj z) (w : { w : Fin S.n // ¬CategoryTheory.Projective (S.fgObj w) }) (hwz : ↑w ≤ z) : S.rightMeshSourceMap H (fun {i j : Fin S.n} => S.replaceArrowMapAt (fun {i j : Fin S.n} => arrowMap) z g) w = S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) w

Updating a later target leaves the paired source map of every earlier nonprojective mesh unchanged.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.lift_map_meshRelation_eq_source_comp_sink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map ((S.rightMeshData H).meshRelation (S.rightMeshNonprojectiveVertex H z)) = CategoryTheory.CategoryStruct.comp (S.rightMeshSourceMap H (fun {i j : Fin S.n} => arrowMap) z) (S.realizedRightMeshSink (fun {i j : Fin S.n} => arrowMap) ↑z)

Evaluation of the literal mesh relation is the recursively assembled source map followed by the sink assembled from the incoming representatives. The equality retains the full occurrence indexing on both sides.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_freePath_map_eq_of_rightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (arrowMap : {i j : Fin S.n} → S.MeshArrow i j → (S.almostSplitSkeleton.obj j ⟶ S.almostSplitSkeleton.obj i)) (z x : Fin S.n) (hsink : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.realizedRightMeshSink (fun {i j : Fin S.n} => arrowMap) z)) (hfull : ∀ y < z, ∀ (f : S.almostSplitSkeleton.obj x ⟶ S.almostSplitSkeleton.obj y), ∃ (p : LinearPathCategory.obj k (Fin S.n) x ⟶ LinearPathCategory.obj k (Fin S.n) y), (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map p = f) (f : S.almostSplitSkeleton.obj x ⟶ S.almostSplitSkeleton.obj z) : ∃ (p : LinearPathCategory.obj k (Fin S.n) x ⟶ LinearPathCategory.obj k (Fin S.n) z), (LinearPathCategory.lift S.almostSplitSkeleton.obj fun {i j : Fin S.n} => arrowMap).map p = f

If the displayed incoming-arrow family realizes a right almost-split sink and the free-path realization is full at every strict predecessor of z, it is full at z as well.