localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG
theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG :
∀ {R : Type u} [inst : CommRing R] {I J : Ideal R}, I ≤ J.radical → J.radical.FG → ∃ k, I ^ k ≤ J
This theorem is about ideals in a commutative ring `R`. Specifically, it states that for any two ideals `I` and `J` in `R`, if `I` is a subset of the radical of `J` and the radical of `J` is finitely generated, then there exists a non-negative integer `k` such that `I` raised to the power of `k` is a subset of `J`. This theorem generalizes the `Ideal.exists_radical_pow_le_of_fg` and suggests that this theorem should be moved to `Mathlib/RingTheory/Finiteness` for closer relation.
More concisely: If `I` is an ideal contained in the radical of the finitely generated ideal `J` in a commutative ring, then there exists a non-negative integer `k` such that `I^k` is contained in `J`.
|
localCohomology.hasColimitDiagram
theorem localCohomology.hasColimitDiagram :
∀ {R : Type (max u v)} [inst : CommRing R] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
(I : CategoryTheory.Functor D (Ideal R)) (i : ℕ),
CategoryTheory.Limits.HasColimit (localCohomology.diagram I i)
The theorem `localCohomology.hasColimitDiagram` states that for any commutative ring `R`, any small category `D`, any functor `I` from `D` to the ideals of `R`, and any natural number `i`, the functor `localCohomology.diagram I i` has a colimit in the category of functors from the opposite of `D` to the category of functors from the module category over `R` to itself. In other words, the directed system of ring module ideals determined by the functor `I` and indexed by the natural number `i` always has a colimit.
More concisely: For any commutative ring R, small category D, and functor I from D to the ideals of R, the functor localCohomology.diagram I i from the opposite of D to the category of R-module functors has a colimit.
|