Indices of ideals

Main result

• Submodule.finite_quotient_smul: Let N be a finite index f.g. R-submodule, and I be a finite index ideal. Then I • N also has finite index.
• Ideal.index_quotient_pow_le: If I is generated by k elements, the index of I ^ n is bounded by #(R ⧸ I) ^ (k⁰ + k¹ + ⋯ + kⁿ⁻¹).

theorem Submodule.finite_quotient_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {N : Submodule R M} [Finite (R ⧸ I)] [Finite (M ⧸ N)] (hN : N.FG) : Finite (M ⧸ I • N)

Let N be a finite index f.g. R-submodule, and I be a finite index ideal. Then I • N also has finite index.

theorem Submodule.index_smul_le {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {N : Submodule R M} [Finite (R ⧸ I)] (s : Finset M) (hs : span R ↑s = N) : (I • N).toAddSubgroup.index ≤ (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

theorem Ideal.finite_quotient_prod {R : Type u_1} [CommRing R] {ι : Type u_3} (I : ι → Ideal R) (s : Finset ι) (hI : ∀ i ∈ s, (I i).FG) (hI' : ∀ i ∈ s, Finite (R ⧸ I i)) : Finite (R ⧸ ∏ i ∈ s, I i)

theorem Ideal.finite_quotient_pow {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I.FG) [Finite (R ⧸ I)] (n : ℕ) : Finite (R ⧸ I ^ n)

theorem Ideal.index_pow_le {R : Type u_1} [CommRing R] {I : Ideal R} (s : Finset R) (hs : span ↑s = I) [Finite (R ⧸ I)] (n : ℕ) : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i