Upper and lower covers in the Boolean algebra B_n

def InvariantPreserve.upperCovers (n : ℕ) (S : Finset (Fin n)) : Finset (Finset (Fin n))

The set of upper covers of S in B_n: all (#S + 1)-element subsets that strictly contain S.

def InvariantPreserve.lowerCovers (n : ℕ) (T : Finset (Fin n)) : Finset (Finset (Fin n))

The set of lower covers of T in B_n: all (#T - 1)-element subsets strictly contained in T.

The raising and lowering operators on basis elements

noncomputable def InvariantPreserve.raisingOnBasis (n : ℕ) (S : Finset (Fin n)) : Finset (Fin n) →₀ ℝ

The raising operator on a basis element: U(e_S) = ∑_{T ⋗ S} e_T, where the sum ranges over all upper covers of S.

noncomputable def InvariantPreserve.loweringOnBasis (n : ℕ) (T : Finset (Fin n)) : Finset (Fin n) →₀ ℝ

The lowering operator on a basis element: D(e_T) = ∑_{S ⋖ T} e_S, where the sum ranges over all lower covers of T.

The raising and lowering operators as linear maps

noncomputable def InvariantPreserve.raisingOp (n : ℕ) : (Finset (Fin n) →₀ ℝ) →ₗ[ℝ] Finset (Fin n) →₀ ℝ

The raising operator U : ℝ^{B_n} → ℝ^{B_n}, extended linearly from the basis action. For a basis element e_S, U(e_S) = ∑_{T : T ⋗ S} e_T.

noncomputable def InvariantPreserve.loweringOp (n : ℕ) : (Finset (Fin n) →₀ ℝ) →ₗ[ℝ] Finset (Fin n) →₀ ℝ

The lowering operator D : ℝ^{B_n} → ℝ^{B_n}, extended linearly from the basis action. For a basis element e_T, D(e_T) = ∑_{S : S ⋖ T} e_S.

Simp lemmas for the operators on single basis elements

@[simp]

theorem InvariantPreserve.raisingOp_single (n : ℕ) (S : Finset (Fin n)) (r : ℝ) : (raisingOp n) (Finsupp.single S r) = r • raisingOnBasis n S

@[simp]

theorem InvariantPreserve.loweringOp_single (n : ℕ) (T : Finset (Fin n)) (r : ℝ) : (loweringOp n) (Finsupp.single T r) = r • loweringOnBasis n T

Group action on ℝ^{B_n} via comapSMul

Custom helpers for comapSMul that don't rely on instance resolution

@[simp]

theorem InvariantPreserve.comapSMul_eq_mapDomain (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (v : Finset (Fin n) →₀ ℝ) : g • v = Finsupp.mapDomain (fun (x : Finset (Fin n)) => g • x) v

comapSMul unfolds to mapDomain by the inverse action. This is definitional.

@[simp]

theorem InvariantPreserve.comapSMul_zero (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) : g • 0 = 0

comapSMul distributes over zero.

@[simp]

theorem InvariantPreserve.comapSMul_add (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (v w : Finset (Fin n) →₀ ℝ) : g • (v + w) = g • v + g • w

comapSMul distributes over addition.

@[simp]

theorem InvariantPreserve.comapSMul_smul (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (r : ℝ) (v : Finset (Fin n) →₀ ℝ) : g • r • v = r • g • v

comapSMul commutes with scalar multiplication by reals.

Group action preserves covering relations

theorem InvariantPreserve.smul_ssubset (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (S T : Finset (Fin n)) (h : S ⊂ T) : g • S ⊂ g • T

A group element preserves strict subset relations on finsets.

theorem InvariantPreserve.smul_upperCovers (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (S : Finset (Fin n)) : Finset.image (fun (x : Finset (Fin n)) => g • x) (upperCovers n S) = upperCovers n (g • S)

A group element maps upper covers of S to upper covers of g • S.

theorem InvariantPreserve.smul_lowerCovers (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (T : Finset (Fin n)) : Finset.image (fun (x : Finset (Fin n)) => g • x) (lowerCovers n T) = lowerCovers n (g • T)

A group element maps lower covers of T to lower covers of g • T.

The group action commutes with the raising/lowering operators on basis elements

theorem InvariantPreserve.smul_raisingOnBasis (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (S : Finset (Fin n)) : Finsupp.mapDomain (fun (x : Finset (Fin n)) => g • x) (raisingOnBasis n S) = raisingOnBasis n (g • S)

The group action on ℝ^{B_n} commutes with raisingOnBasis on single basis elements: g • U(e_S) = U(e_{g • S}).

theorem InvariantPreserve.smul_loweringOnBasis (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (T : Finset (Fin n)) : Finsupp.mapDomain (fun (x : Finset (Fin n)) => g • x) (loweringOnBasis n T) = loweringOnBasis n (g • T)

The group action on ℝ^{B_n} commutes with loweringOnBasis on single basis elements: g • D(e_T) = D(e_{g • T}).

Full commutativity: g • U(v) = U(g • v) for all v

theorem InvariantPreserve.raisingOp_comm_smul (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (v : Finset (Fin n) →₀ ℝ) : g • (raisingOp n) v = (raisingOp n) (g • v)

The raising operator commutes with the group action: g • U(v) = U(g • v) for all v ∈ ℝ^{B_n}. This follows from linearity and commutativity on basis elements.

theorem InvariantPreserve.loweringOp_comm_smul (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (g : G) (v : Finset (Fin n) →₀ ℝ) : g • (loweringOp n) v = (loweringOp n) (g • v)

The lowering operator commutes with the group action: g • D(v) = D(g • v) for all v ∈ ℝ^{B_n}.

Main theorem: U and D preserve the G-invariant subspace

theorem InvariantPreserve.linearMap_preserves_invariant (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (f : (Finset (Fin n) →₀ ℝ) →ₗ[ℝ] Finset (Fin n) →₀ ℝ) (hcomm : ∀ (g : G) (v : Finset (Fin n) →₀ ℝ), g • f v = f (g • v)) {v : Finset (Fin n) →₀ ℝ} (hv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) : f v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))

A general lemma: if a linear map commutes with the group action, then it preserves the invariant subspace.

theorem InvariantPreserve.raisingOp_mem_invariantSubspace (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] {v : Finset (Fin n) →₀ ℝ} (hv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) : (raisingOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))

Lemma 5.8 (part 1). If v is in the G-invariant subspace ℝ(B_n)^G, then U(v) is also in ℝ(B_n)^G. The raising operator preserves the invariant subspace. (Lemma 5.8, Stanley's Algebraic Combinatorics)

theorem InvariantPreserve.loweringOp_mem_invariantSubspace (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] {v : Finset (Fin n) →₀ ℝ} (hv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) : (loweringOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))

Lemma 5.8 (part 2). If v is in the G-invariant subspace ℝ(B_n)^G, then D(v) is also in ℝ(B_n)^G. The lowering operator preserves the invariant subspace. (Lemma 5.8, Stanley's Algebraic Combinatorics)

Graded structure: the raising and lowering operators respect level

theorem InvariantPreserve.raisingOnBasis_support_subset (n : ℕ) (S : Finset (Fin n)) : (raisingOnBasis n S).support ⊆ upperCovers n S

The support of raisingOnBasis n S is contained in upperCovers n S.

theorem InvariantPreserve.loweringOnBasis_support_subset (n : ℕ) (T : Finset (Fin n)) : (loweringOnBasis n T).support ⊆ lowerCovers n T

The support of loweringOnBasis n T is contained in lowerCovers n T.

theorem InvariantPreserve.card_of_mem_upperCovers (n : ℕ) {S T : Finset (Fin n)} (hT : T ∈ upperCovers n S) : T.card = S.card + 1

Elements in upperCovers n S have cardinality S.card + 1.

theorem InvariantPreserve.card_of_mem_lowerCovers (n : ℕ) {S T : Finset (Fin n)} (hS : S ∈ lowerCovers n T) : S.card + 1 = T.card

Elements in lowerCovers n T have cardinality one less: S.card + 1 = T.card.

theorem InvariantPreserve.raisingOp_support_card (n i : ℕ) (v : Finset (Fin n) →₀ ℝ) (hv : ∀ x ∈ v.support, x.card = i) (y : Finset (Fin n)) : y ∈ ((raisingOp n) v).support → y.card = i + 1

The raising operator maps level-i elements to level-(i+1) elements: if v is supported on sets of cardinality i, then raisingOp n v is supported on sets of cardinality i + 1.

theorem InvariantPreserve.loweringOp_support_card (n i : ℕ) (v : Finset (Fin n) →₀ ℝ) (hv : ∀ x ∈ v.support, x.card = i) (y : Finset (Fin n)) : y ∈ ((loweringOp n) v).support → y.card + 1 = i

The lowering operator maps level-i elements to level-(i-1) elements: if v is supported on sets of cardinality i, then loweringOp n v is supported on sets of cardinality i - 1, expressed as y.card + 1 = i.

theorem InvariantPreserve.raisingOp_preserves_graded_invariant (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (i : ℕ) (v : Finset (Fin n) →₀ ℝ) (hv_level : ∀ x ∈ v.support, x.card = i) (hv_inv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) : (∀ y ∈ ((raisingOp n) v).support, y.card = i + 1) ∧ (raisingOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))

Lemma 5.8 (Graded, raising). The raising operator maps level-i G-invariant elements to level-(i+1) G-invariant elements. If v is supported on B_n elements of grade i and is G-invariant, then U(v) is supported on elements of grade i+1 and is G-invariant. (Lemma 5.8, Stanley's Algebraic Combinatorics)

theorem InvariantPreserve.loweringOp_preserves_graded_invariant (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] (i : ℕ) (v : Finset (Fin n) →₀ ℝ) (hv_level : ∀ x ∈ v.support, x.card = i) (hv_inv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) : (∀ y ∈ ((loweringOp n) v).support, y.card + 1 = i) ∧ (loweringOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))

Lemma 5.8 (Graded, lowering). The lowering operator maps level-i G-invariant elements to level-(i-1) G-invariant elements. If v is supported on B_n elements of grade i and is G-invariant, then D(v) is supported on elements of grade i-1 and is G-invariant. (Lemma 5.8, Stanley's Algebraic Combinatorics)

supportedAtLevel predicate: bundled graded component membership

def InvariantPreserve.supportedAtLevel (n i : ℕ) (v : Finset (Fin n) →₀ ℝ) : Prop

A vector v ∈ ℝ^{B_n} is supported at level i if every finset in the support of v has cardinality i. This captures membership in the i-th graded component ℝ(B_n)_i.

theorem InvariantPreserve.raisingOp_supportedAtLevel (n : ℕ) {i : ℕ} {v : Finset (Fin n) →₀ ℝ} (hv : supportedAtLevel n i v) : supportedAtLevel n (i + 1) ((raisingOp n) v)

The raising operator maps vectors supported at level i to vectors supported at level i + 1.

theorem InvariantPreserve.loweringOp_supportedAtLevel (n : ℕ) {i : ℕ} {v : Finset (Fin n) →₀ ℝ} (hv : supportedAtLevel n i v) : supportedAtLevel n (i - 1) ((loweringOp n) v)

The lowering operator maps vectors supported at level i to vectors supported at level i - 1.

theorem InvariantPreserve.raisingOp_mem_invariantSubspace_graded (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] {v : Finset (Fin n) →₀ ℝ} {i : ℕ} (hv_inv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) (hv_level : supportedAtLevel n i v) : (raisingOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n)) ∧ supportedAtLevel n (i + 1) ((raisingOp n) v)

Lemma 5.8 (graded, part 1). If v ∈ ℝ(B_n)_i^G (i.e., v is G-invariant and supported at level i), then U_i(v) ∈ ℝ(B_n)_{i+1}^G (i.e., U(v) is G-invariant and supported at level i + 1).

theorem InvariantPreserve.loweringOp_mem_invariantSubspace_graded (n : ℕ) (G : Type u_1) [Group G] [MulAction G (Fin n)] {v : Finset (Fin n) →₀ ℝ} {i : ℕ} (hv_inv : v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n))) (hv_level : supportedAtLevel n i v) : (loweringOp n) v ∈ OrbitBasis.invariantSubspace G (Finset (Fin n)) ∧ supportedAtLevel n (i - 1) ((loweringOp n) v)

Lemma 5.8 (graded, part 2). If v ∈ ℝ(B_n)_i^G (i.e., v is G-invariant and supported at level i), then D(v) ∈ ℝ(B_n)_{i-1}^G (i.e., D(v) is G-invariant and supported at level i - 1).