Commit 2026-03-05 10:25 2e7b7491

View on Github →

feat(RingTheory): define maps of homogeneous ideals (#30334) In this file we define HomogeneousIdeal.map and HomogeneousIdeal.comap, similar to and based on the existing Ideal.map and Ideal.comap. More concretely, a graded ring homomorphism 𝒜 →+*ᵍ ℬ induces a "Galois connection" between the homogeneous ideals in 𝒜 and the homogeneous ideals in ℬ.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

added theorem coe_toIdeal

added theorem toIdeal_le_toIdeal_iff

Created Mathlib/RingTheory/GradedAlgebra/Homogeneous/Maps.lean

added theorem HomogeneousIdeal.coe_comap

added def HomogeneousIdeal.comap

added theorem HomogeneousIdeal.comap_comap

added theorem HomogeneousIdeal.comap_id

added theorem HomogeneousIdeal.comap_mono

added theorem HomogeneousIdeal.gc_map_comap

added def HomogeneousIdeal.map

added theorem HomogeneousIdeal.map_comp

added theorem HomogeneousIdeal.map_id

added theorem HomogeneousIdeal.map_le_iff_le_comap

added theorem HomogeneousIdeal.map_map

added theorem HomogeneousIdeal.map_mono

added theorem HomogeneousIdeal.toIdeal_comap

added theorem HomogeneousIdeal.toIdeal_map