Graded poset spaces

This file isolates the linear-algebra step in the frozen manuscript's grading argument. An internal grading of the total space of a poset representation is compatible when every distinguished subspace is closed under the homogeneous projections. For a Schur poset space those projections are scalar endomorphisms, so exactly one homogeneous component can be nonzero.

The generic one-dimensional lemma is also recorded separately. It is the tool used for the one-dimensional spaces Hom(P, P_t) in the projective boundary realization.

theorem MagnitudeConjecture.GradedLinear.existsUnique_component_eq_top_of_finrank_eq_one {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V] {ι : Type w} [DecidableEq ι] (A : ι → Submodule k V) (hA : DirectSum.IsInternal A) (hfin : Module.finrank k V = 1) : ∃! i : ι, A i = ⊤

A one-dimensional internally graded vector space has exactly one nonzero component, and that component is the whole space.

theorem MagnitudeConjecture.GradedLinear.existsUnique_mem_of_finrank_eq_one {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V] {ι : Type w} [DecidableEq ι] (A : ι → Submodule k V) (hA : DirectSum.IsInternal A) (hfin : Module.finrank k V = 1) {v : V} (hv : v ≠ 0) : ∃! i : ι, v ∈ A i

Every nonzero vector in a one-dimensional internally graded vector space lies in a unique homogeneous component.

def MagnitudeConjecture.GradedLinear.ShiftsDegree {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V] {W : Type w} [AddCommGroup W] [Module k W] (A : ℕ → Submodule k V) (B : ℕ → Submodule k W) (f : V →ₗ[k] W) (d : ℕ) : Prop

A linear map shifts an ℕ-grading by d when it sends the degree-i component into degree i + d.

theorem MagnitudeConjecture.GradedLinear.ShiftsDegree.range_isHomogeneous {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V] {W : Type w} [AddCommGroup W] [Module k W] (A : ℕ → Submodule k V) (B : ℕ → Submodule k W) (hA : DirectSum.IsInternal A) (hB : DirectSum.IsInternal B) (f : V →ₗ[k] W) {d : ℕ} (hf : ShiftsDegree A B f d) : DirectSum.SetLike.IsHomogeneous B f.range

The range of a degree-shifting linear map is homogeneous in the target grading.

structure MagnitudeConjecture.PosetSpace.InternalGrading {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) : Type u

An internal grading of a poset space whose degree projections preserve all distinguished subspaces.

• component : ℕ → Submodule k X.carrier
• isInternal : DirectSum.IsInternal self.component
• subspace_isHomogeneous (t : T) : DirectSum.SetLike.IsHomogeneous self.component (X.subspace t)

noncomputable def MagnitudeConjecture.PosetSpace.InternalGrading.projection {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (i : ℕ) : X ⟶ X

Projection onto one homogeneous component, regarded as a poset-space endomorphism.

@[simp]

theorem MagnitudeConjecture.PosetSpace.InternalGrading.projection_apply {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (i : ℕ) (x : X.carrier) : (G.projection i).linear x = ↑(((DirectSum.decompose G.component) x) i)

theorem MagnitudeConjecture.PosetSpace.InternalGrading.exists_component_ne_bot {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hne : ∃ (x : X.carrier), x ≠ 0) : ∃ (i : ℕ), G.component i ≠ ⊥

theorem MagnitudeConjecture.PosetSpace.InternalGrading.component_eq_top_of_ne_bot_of_isSchur {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) (i : ℕ) (hi : G.component i ≠ ⊥) : G.component i = ⊤

theorem MagnitudeConjecture.PosetSpace.InternalGrading.existsUnique_component_eq_top {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) : ∃! i : ℕ, G.component i = ⊤

A Schur poset space carrying a compatible internal grading is concentrated in one unique degree.

noncomputable def MagnitudeConjecture.PosetSpace.InternalGrading.level {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) : ℕ

The unique degree containing a compatibly graded Schur poset space.

@[simp]

theorem MagnitudeConjecture.PosetSpace.InternalGrading.component_level_eq_top {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) : G.component (G.level hX) = ⊤

theorem MagnitudeConjecture.PosetSpace.InternalGrading.eq_level_of_component_eq_top {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) {i : ℕ} (hi : G.component i = ⊤) : i = G.level hX

theorem MagnitudeConjecture.PosetSpace.InternalGrading.component_eq_bot_of_ne_level {k T : Type u} [Field k] [PartialOrder T] {X : Obj k T} (G : InternalGrading X) (hX : IsSchur k T X) {i : ℕ} (hi : i ≠ G.level hX) : G.component i = ⊥

def MagnitudeConjecture.PosetSpace.InternalGrading.HomogeneousOfDegree {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (GX : InternalGrading X) (GY : InternalGrading Y) (f : X ⟶ Y) (d : ℕ) : Prop

A morphism is homogeneous of degree d when it sends degree i into degree i + d.

theorem MagnitudeConjecture.PosetSpace.InternalGrading.level_add_degree_eq {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (GX : InternalGrading X) (GY : InternalGrading Y) (hX : IsSchur k T X) (hY : IsSchur k T Y) {f : X ⟶ Y} {d : ℕ} (hf : f ≠ 0) (hhom : GX.HomogeneousOfDegree GY f d) : GX.level hX + d = GY.level hY

A nonzero homogeneous morphism between compatibly graded Schur poset spaces identifies the target level with source level plus its degree.

theorem MagnitudeConjecture.PosetSpace.InternalGrading.level_lt_of_homogeneousOfDegree {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (GX : InternalGrading X) (GY : InternalGrading Y) (hX : IsSchur k T X) (hY : IsSchur k T Y) {f : X ⟶ Y} {d : ℕ} (hf : f ≠ 0) (hd : 0 < d) (hhom : GX.HomogeneousOfDegree GY f d) : GX.level hX < GY.level hY

A nonzero homogeneous morphism of positive degree strictly raises the concentration level.