Endomorphism stabilizers of subspace filtrations

This file gives the dimension-intersection argument needed for the manuscript's two-filtration step. It reduces the Schur-dimension conclusion to lower bounds for the stabilizers of the two individual chains.

def MagnitudeConjecture.PosetSpace.TriangularIndex (n : ℕ) : Type

Upper-triangular matrix-unit indices: (i,j) with i ≤ j.

def MagnitudeConjecture.PosetSpace.triangularIndexEquivSigma (n : ℕ) : TriangularIndex n ≃ (j : Fin n) × Fin (↑j + 1)

Triangular indices are equivalently a column j together with a row in Fin (j+1).

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instFintypeTriangularIndex (n : ℕ) : Fintype (TriangularIndex n)

theorem MagnitudeConjecture.PosetSpace.two_mul_card_triangularIndex (n : ℕ) : 2 * Fintype.card (TriangularIndex n) = n * (n + 1)

Twice the number of triangular matrix units is n(n+1).

noncomputable def MagnitudeConjecture.PosetSpace.triangularEnd {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) (p : TriangularIndex n) : V →ₗ[k] V

The triangular matrix units attached to a basis.

def MagnitudeConjecture.PosetSpace.triangularEndSpan {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) : Submodule k (Module.End k V)

The subspace of endomorphisms spanned by the triangular matrix units.

theorem MagnitudeConjecture.PosetSpace.linearIndependent_triangularEnd {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) : LinearIndependent k (triangularEnd b)

The triangular matrix units are linearly independent.

theorem MagnitudeConjecture.PosetSpace.finrank_triangularEndSpan {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) : Module.finrank k ↥(triangularEndSpan b) = Fintype.card (TriangularIndex n)

The triangular endomorphism subspace has the expected dimension.

theorem MagnitudeConjecture.PosetSpace.triangularEnd_preserves_flag {k : Type u} [Field k] {V : Type u} [AddCommGroup V] [Module k V] {n : ℕ} (b : Module.Basis (Fin n) k V) (p : TriangularIndex n) (m : Fin (n + 1)) {x : V} (hx : x ∈ b.flag m) : (triangularEnd b p) x ∈ b.flag m

Every upper-triangular matrix unit preserves every flag subspace of its basis.

def MagnitudeConjecture.PosetSpace.HasFlagBasisOn {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (S : Set T) : Prop

The subspaces indexed by S form subspaces in a single complete flag.

def MagnitudeConjecture.PosetSpace.stabilizerOn {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (S : Set T) : Submodule k (X.carrier →ₗ[k] X.carrier)

Linear endomorphisms preserving the distinguished subspaces indexed by the set S.

@[simp]

theorem MagnitudeConjecture.PosetSpace.mem_stabilizerOn_iff {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (S : Set T) (f : X.carrier →ₗ[k] X.carrier) : f ∈ stabilizerOn X S ↔ ∀ t ∈ S, ∀ x ∈ X.subspace t, f x ∈ X.subspace t

theorem MagnitudeConjecture.PosetSpace.triangularEndSpan_le_stabilizerOn {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (S : Set T) (b : Module.Basis (Fin (Module.finrank k X.carrier)) k X.carrier) (hb : ∀ t ∈ S, ∃ (m : Fin (Module.finrank k X.carrier + 1)), X.subspace t = b.flag m) : triangularEndSpan b ≤ stabilizerOn X S

The triangular endomorphism subspace attached to a flag basis lies in the stabilizer of all subspaces belonging to that flag.

theorem MagnitudeConjecture.PosetSpace.card_triangularIndex_le_finrank_stabilizerOn {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (S : Set T) (hflag : HasFlagBasisOn X S) : Fintype.card (TriangularIndex (Module.finrank k X.carrier)) ≤ Module.finrank k ↥(stabilizerOn X S)

A family of subspaces contained in one complete flag has a stabilizer of dimension at least n(n+1)/2.

theorem MagnitudeConjecture.PosetSpace.stabilizerOn_union {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (A B : Set T) : stabilizerOn X (A ∪ B) = stabilizerOn X A ⊓ stabilizerOn X B

Preserving a union of index sets is the intersection of the two stabilizer subspaces.

def MagnitudeConjecture.PosetSpace.homOfMemStabilizerOnUniv {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (f : ↥(stabilizerOn X Set.univ)) : X ⟶ X

An element of the full stabilizer is an endomorphism of the poset space.

theorem MagnitudeConjecture.PosetSpace.finrank_stabilizerOn_univ_le_one_of_isSchur {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) : Module.finrank k ↥(stabilizerOn X Set.univ) ≤ 1

The full stabilizer of a Schur poset space has dimension at most one.

theorem MagnitudeConjecture.PosetSpace.two_le_finrank_stabilizerOn_union {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (A B : Set T) (hlarge : Module.finrank k (X.carrier →ₗ[k] X.carrier) + 2 ≤ Module.finrank k ↥(stabilizerOn X A) + Module.finrank k ↥(stabilizerOn X B)) : 2 ≤ Module.finrank k ↥(stabilizerOn X (A ∪ B))

If two partial stabilizers are jointly larger than the ambient endomorphism space by at least two dimensions, then their intersection has dimension at least two.

theorem MagnitudeConjecture.PosetSpace.finrank_le_one_of_isSchur_of_two_stabilizer_bounds {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) (A B : Set T) (hcover : A ∪ B = Set.univ) (hlarge : 2 ≤ Module.finrank k X.carrier → Module.finrank k (X.carrier →ₗ[k] X.carrier) + 2 ≤ Module.finrank k ↥(stabilizerOn X A) + Module.finrank k ↥(stabilizerOn X B)) : Module.finrank k X.carrier ≤ 1

Dimension bounds for two covering filtration stabilizers force a Schur poset space to have dimension at most one.

theorem MagnitudeConjecture.PosetSpace.two_flag_bases_stabilizer_bound {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (A B : Set T) (hA : HasFlagBasisOn X A) (hB : HasFlagBasisOn X B) (hrank : 2 ≤ Module.finrank k X.carrier) : Module.finrank k (X.carrier →ₗ[k] X.carrier) + 2 ≤ Module.finrank k ↥(stabilizerOn X A) + Module.finrank k ↥(stabilizerOn X B)

Two flag-indexed covering families give the stabilizer dimension bound needed in the Schur argument.

theorem MagnitudeConjecture.PosetSpace.finrank_le_one_of_isSchur_of_two_flag_bases {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) (A B : Set T) (hcover : A ∪ B = Set.univ) (hA : HasFlagBasisOn X A) (hB : HasFlagBasisOn X B) : Module.finrank k X.carrier ≤ 1

A Schur poset space whose distinguished subspaces are covered by two complete flags has total dimension at most one.

theorem MagnitudeConjecture.PosetSpace.finrank_eq_one_of_isSchur_of_two_flag_bases {k T : Type u} [Field k] [PartialOrder T] (X : Obj k T) (hschur : IsSchur k T X) (A B : Set T) (hcover : A ∪ B = Set.univ) (hA : HasFlagBasisOn X A) (hB : HasFlagBasisOn X B) : Module.finrank k X.carrier = 1

In particular, a nonzero Schur poset space covered by two flag-indexed families is one-dimensional.