Kernels lemma for coprime polynomials

TheoremKernel of a product of pairwise coprime polynomials#✓fully proved

Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(f\) an \(R\)-linear endomorphism of \(M\), and \((p_i)_{i \in \iota}\) a family of polynomials in \(R[X]\) that are pairwise coprime, meaning that for all \(i \ne j\) there are \(a, b \in R[X]\) with \(a p_i + b p_j = 1\). Then for every finite set \(s \subseteq \iota\), the sum of the submodules \(\ker p_i(f)\) over \(i \in s\) equals \(\ker \bigl(\prod_{i \in s} p_i\bigr)(f)\).

theorem iSup_ker_aeval_eq_ker_aeval_prod_of_pairwise_isCoprime {ι : Type*}
    (f : Module.End R M) (p : ι → R[X])
    (hcop : Pairwise fun i j => IsCoprime (p i) (p j)) (s : Finset ι) :
    (⨆ i ∈ s, LinearMap.ker (aeval f (p i))) =
      LinearMap.ker (aeval f (∏ i ∈ s, p i))

Used by 2

Used byIndependence and sum of kernels of pairwise coprime polynomials · Kernels of pairwise coprime polynomials are independent over a finite set

TheoremKernels of pairwise coprime polynomials are independent over a finite set#✓fully proved

Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(f\) an \(R\)-linear endomorphism of \(M\), and \((p_i)_{i \in \iota}\) a family of polynomials in \(R[X]\) that are pairwise coprime, meaning that for all \(i \ne j\) there are \(a, b \in R[X]\) with \(a p_i + b p_j = 1\). Then for every finite set \(s \subseteq \iota\), every \(i \in s\) and every \(t \subseteq s\) with \(i \notin t\), the submodule \(\ker p_i(f)\) meets the sum of the submodules \(\ker p_j(f)\) over \(j \in t\) only in \(0\).

theorem supIndep_ker_aeval_of_pairwise_isCoprime {ι : Type*}
    (f : Module.End R M) (p : ι → R[X])
    (hcop : Pairwise fun i j => IsCoprime (p i) (p j)) (s : Finset ι) :
    s.SupIndep fun i => LinearMap.ker (aeval f (p i))

Uses 1 · Used by 1

Proof usesKernel of a product of pairwise coprime polynomials

Used byIndependence and sum of kernels of pairwise coprime polynomials

TheoremIndependence and sum of kernels of pairwise coprime polynomials#✓fully proved

Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(f\) an \(R\)-linear endomorphism of \(M\), and \((p_i)_{i \in \iota}\) a family of polynomials in \(R[X]\), indexed by a finite type \(\iota\), that are pairwise coprime, meaning that for all \(i \ne j\) there are \(a, b \in R[X]\) with \(a p_i + b p_j = 1\). Then the submodules \(\ker p_i(f)\) are independent (each meets the sum of the others only in \(0\)), and their sum is \(\ker \bigl(\prod_{i \in \iota} p_i\bigr)(f)\).

theorem iSupIndep_ker_aeval_and_iSup_eq_of_pairwise_isCoprime {ι : Type*} [Fintype ι]
    (f : Module.End R M) (p : ι → R[X])
    (hcop : Pairwise fun i j => IsCoprime (p i) (p j)) :
    iSupIndep (fun i => LinearMap.ker (aeval f (p i))) ∧
      (⨆ i, LinearMap.ker (aeval f (p i))) = LinearMap.ker (aeval f (∏ i, p i))

Uses 2 · Used by 1

Proof usesKernel of a product of pairwise coprime polynomials · Kernels of pairwise coprime polynomials are independent over a finite set

Used byKernels lemma

TheoremKernels lemma#✓fully proved

Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(f\) an \(R\)-linear endomorphism of \(M\), and \((p_i)_{i \in \iota}\) a family of polynomials in \(R[X]\), indexed by a finite type \(\iota\), that are pairwise coprime, meaning that for all \(i \ne j\) there are \(a, b \in R[X]\) with \(a p_i + b p_j = 1\). Then the submodules \(\ker p_i(f)\) are independent (each meets the sum of the others only in \(0\)), and their sum is \(\ker \bigl(\prod_{i \in \iota} p_i\bigr)(f)\).

The decomposition is internal to \(\ker \bigl(\prod_{i \in \iota} p_i\bigr)(f)\); it need not span all of \(M\).

Proof: induction on the number of polynomials from the two-polynomial case, as in the cited French Wikipedia article. For coprime \(p\) and \(q\) one has \(\ker p(f) + \ker q(f) = \ker (pq)(f)\), which gives the inductive step, and independence follows because \(\ker p_i(f) \cap \ker q(f) = 0\) when \(q\) is the product of the other polynomials.

theorem kernels_lemma_pairwise_isCoprime {ι : Type*} [Fintype ι]
    (f : Module.End R M) (p : ι → R[X])
    (hcop : Pairwise fun i j => IsCoprime (p i) (p j)) :
    iSupIndep (fun i => LinearMap.ker (aeval f (p i))) ∧
      (⨆ i, LinearMap.ker (aeval f (p i))) = LinearMap.ker (aeval f (∏ i, p i))

Sources

• https://fr.wikipedia.org/wiki/Lemme_des_noyaux; S. Axler, Linear Algebra Done Right, 4th ed., Springer (2024), Section 8C.

Uses 1

Proof usesIndependence and sum of kernels of pairwise coprime polynomials

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.