Supports, splittings, determinants and coordinate separation for dependent products

For s : Set ι, the submodule Submodule.pi sᶜ (fun _ ↦ ⊥) of ∀ i, M i consists of the families vanishing outside s, the Pi analogue of Finsupp.supported; such submodules for disjoint supports meet in ⊥. This file also records the linear splitting of a dependent product along a predicate on the indices, the linear splitting of a Fin (n + 1)-indexed product into its initial segment and its last coordinate, and the determinant of a coordinatewise endomorphism of a finite dependent product, which is used in finite-product norm calculations.

Finally, distinct sums and differences of standard coordinate vectors can be separated at a coordinate where their difference is regular. In two of these separations the critical case is one family being the negative of the other, so that their difference is 2 times a vector of ±1s; those two assume 2 is regular, while separating two unordered sums needs no such hypothesis. These elementary facts are useful for identifying root spaces from their coordinate weights.

Main results

• Submodule.disjoint_pi_compl_bot_of_disjoint: disjoint index sets give disjoint submodules of families vanishing outside them.
• LinearEquiv.piFinSnoc: the linear splitting of a tuple of length n + 1 into its initial n coordinates and its last one, with Fin.snoc as its inverse.
• Fin.snoc_zero_eq_single: the tuple of length n + 1 with vanishing initial segment is the one-point family Pi.single at the last index.
• LinearEquiv.piEquivPiSubtypeProd: Equiv.piEquivPiSubtypeProd as a linear equivalence, splitting ∀ i, M i into the factors indexed by p and by ¬p.
• LinearMap.toMatrix_piMap: in product bases, LinearMap.piMap f is block diagonal, including when its component maps have different source and target modules.
• LinearMap.det_piMap: the determinant of a coordinatewise endomorphism LinearMap.piMap f of a finite dependent product is the product of the determinants of its components.
• TauCeti.finrank_linearMap_pi_eq_sum: the dimension of maps between finite dependent products is the sum of the dimensions of the component hom spaces.
• TauCeti.exists_isRegular_single_sub_single_sub: an ordered difference of standard coordinate vectors on two different coordinates and any other ordered difference differ regularly at some coordinate.
• TauCeti.exists_isRegular_single_add_single_sub: a sum of standard coordinate vectors on two different coordinates and a sum with a different unordered index pair differ regularly at some coordinate.
• TauCeti.exists_isRegular_neg_single_add_single_sub_single_add_single: a negative coordinate sum and a coordinate sum on two different coordinates differ regularly at some coordinate.

theorem Fin.snoc_zero_eq_single {n : ℕ} {M : Fin (n + 1) → Type u_1} [(i : Fin (n + 1)) → Zero (M i)] (x : M (last n)) : snoc 0 x = Pi.single (last n) x

A tuple with vanishing initial segment is a one-point family. Appending x to the zero tuple of length n gives the family supported at the last index with value x there.

theorem Submodule.disjoint_pi_compl_bot_of_disjoint {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {s t : Set ι} (h : Disjoint s t) : Disjoint (pi sᶜ fun (i : ι) => ⊥) (pi tᶜ fun (i : ι) => ⊥)

Disjoint index sets give disjoint submodules of the families vanishing outside them: a family vanishing outside s and outside t, for s and t disjoint, is zero.

def LinearEquiv.piFinSnoc (R : Type u_1) [Semiring R] {n : ℕ} (M : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] : ((i : Fin (n + 1)) → M i) ≃ₗ[R] ((i : Fin n) → M i.castSucc) × M (Fin.last n)

Splits a tuple of length n + 1 into its initial n coordinates and its last one, with inverse Fin.snoc. This is the inverse of Fin.snocEquiv as a LinearEquiv, with the factors swapped so that the initial segment comes first, matching the argument order of Fin.snoc.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.piFinSnoc_apply (R : Type u_1) [Semiring R] {n : ℕ} (M : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] (v : (i : Fin (n + 1)) → M i) : (piFinSnoc R M) v = (Fin.init v, v (Fin.last n))

@[simp]

theorem LinearEquiv.piFinSnoc_symm_apply (R : Type u_1) [Semiring R] {n : ℕ} (M : Fin (n + 1) → Type u_2) [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] (p : ((i : Fin n) → M i.castSucc) × M (Fin.last n)) : (piFinSnoc R M).symm p = Fin.snoc p.1 p.2

def LinearEquiv.piEquivPiSubtypeProd (R : Type u_1) {ι : Type u_2} [Semiring R] (p : ι → Prop) [DecidablePred p] (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : ((i : ι) → M i) ≃ₗ[R] ((i : { x : ι // p x }) → M ↑i) × ((i : { x : ι // ¬p x }) → M ↑i)

Splits the indices of the module ∀ i, M i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a LinearEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.piEquivPiSubtypeProd_apply (R : Type u_1) {ι : Type u_2} [Semiring R] (p : ι → Prop) [DecidablePred p] (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (f : (i : ι) → M i) : (piEquivPiSubtypeProd R p M) f = (fun (i : { x : ι // p x }) => f ↑i, fun (i : { x : ι // ¬p x }) => f ↑i)

@[simp]

theorem LinearEquiv.piEquivPiSubtypeProd_symm_apply (R : Type u_1) {ι : Type u_2} [Semiring R] (p : ι → Prop) [DecidablePred p] (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (f : ((i : { x : ι // p x }) → M ↑i) × ((i : { x : ι // ¬p x }) → M ↑i)) (i : ι) : (piEquivPiSubtypeProd R p M).symm f i = if h : p i then f.1 ⟨i, h⟩ else f.2 ⟨i, h⟩

theorem LinearMap.toMatrix_piMap {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] {M : ι → Type u_3} {N : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] {κ : ι → Type u_5} {κ' : ι → Type u_6} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] [∀ (i : ι), Finite (κ' i)] (b : (i : ι) → Module.Basis (κ i) R (M i)) (c : (i : ι) → Module.Basis (κ' i) R (N i)) (f : (i : ι) → M i →ₗ[R] N i) : (toMatrix (Pi.basis b) (Pi.basis c)) (piMap f) = Matrix.blockDiagonal' fun (i : ι) => (toMatrix (b i) (c i)) (f i)

In the product bases Pi.basis b and Pi.basis c, the coordinatewise linear map LinearMap.piMap f has the block-diagonal matrix whose blocks are the matrices of the f i. The source and target modules, and hence the row and column index types of each block, may differ.

@[simp]

theorem LinearMap.det_piMap {R : Type u_1} {ι : Type u_2} [CommRing R] [Fintype ι] {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] (f : (i : ι) → M i →ₗ[R] M i) : LinearMap.det (piMap f) = ∏ i : ι, LinearMap.det (f i)

The determinant of the coordinatewise endomorphism LinearMap.piMap f of a finite dependent product of finite free modules is the product of the determinants of the f i. This is the dependent-family version of Mathlib's LinearMap.det_pi.

theorem TauCeti.finrank_linearMap_pi_eq_sum {k : Type u_1} {A : Type u_2} {ι : Type u_3} {κ : Type u_4} [Field k] [Semiring A] [Algebra k A] [Fintype ι] [Fintype κ] (S : ι → Type u_5) (T : κ → Type u_6) [(i : ι) → AddCommMonoid (S i)] [(i : ι) → Module A (S i)] [(j : κ) → AddCommMonoid (T j)] [(j : κ) → Module k (T j)] [(j : κ) → Module A (T j)] [∀ (j : κ), IsScalarTower k A (T j)] [∀ (i : ι) (j : κ), Module.Finite k (S i →ₗ[A] T j)] : Module.finrank k (((i : ι) → S i) →ₗ[A] (j : κ) → T j) = ∑ i : ι, ∑ j : κ, Module.finrank k (S i →ₗ[A] T j)

The dimension of maps between two finite dependent products is the sum of the dimensions of the component hom spaces, provided those hom spaces are finite-dimensional.

theorem TauCeti.exists_isRegular_single_sub_single_sub {K : Type u_1} {ι : Type u_2} [Ring K] [DecidableEq ι] (h2 : IsRegular 2) {i j : ι} (hij : i ≠ j) (a b : ι) (hne : ¬(a = i ∧ b = j)) : ∃ (k : ι), IsRegular ((Pi.single a 1 - Pi.single b 1 - (Pi.single i 1 - Pi.single j 1)) k)

If i ≠ j and the index pair (a, b) differs from (i, j), then the ordered differences of standard coordinate vectors eₐ - e_b and eᵢ - eⱼ differ by a regular scalar at some coordinate, provided 2 is regular.

theorem TauCeti.exists_isRegular_single_add_single_sub {K : Type u_1} {ι : Type u_2} [Ring K] [DecidableEq ι] {i j : ι} (hij : i ≠ j) (a b : ι) (hne : ¬(a = i ∧ b = j ∨ a = j ∧ b = i)) : ∃ (k : ι), IsRegular ((Pi.single a 1 + Pi.single b 1 - (Pi.single i 1 + Pi.single j 1)) k)

If i ≠ j and the unordered index pair {a, b} differs from {i, j}, then the sums of standard coordinate vectors eₐ + e_b and eᵢ + eⱼ differ by a regular scalar at some coordinate.

theorem TauCeti.exists_isRegular_neg_single_add_single_sub_single_add_single {K : Type u_1} {ι : Type u_2} [Ring K] [DecidableEq ι] (h2 : IsRegular 2) {i j : ι} (hij : i ≠ j) (a b : ι) : ∃ (k : ι), IsRegular ((-(Pi.single a 1 + Pi.single b 1) - (Pi.single i 1 + Pi.single j 1)) k)

If i ≠ j, then the negative sum of standard coordinate vectors -(eₐ + e_b) and the sum eᵢ + eⱼ differ by a regular scalar at some coordinate, provided 2 is regular.