Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-25 19:59 5a684ce8

View on Github →

feat(algebra/homology/local_cohomology): just the definition (#19061)

Estimated changes

Modified docs/references.bib

Modified src/algebra/category/Module/colimits.lean

Created src/algebra/homology/local_cohomology.lean

added theorem ideal.exists_pow_le_of_le_radical_of_fg

added def local_cohomology.diagram

added def local_cohomology.ideal_powers_diagram

added def local_cohomology.ideal_powers_to_self_le_radical

added def local_cohomology.ideal_powers_to_self_le_radical_comp_inclusion

added def local_cohomology.of_diagram

added def local_cohomology.of_self_le_radical

added def local_cohomology.ring_mod_ideals

added def local_cohomology.self_le_radical

added def local_cohomology.self_le_radical_diagram

added def local_cohomology