Commit 2026-03-03 16:35 ad4f601c

View on Github →

feat(RingTheory): define graded ring homomorphisms (#30312) This PR defines graded ring homomorphisms, which are ring homomorphisms that preserve the grading. We also provide the basic properties (aka the "API"). Zulip discussion: #mathlib4 > Graded Ring Hom

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/GradedAlgebra/RingHom.lean

added theorem DirectSum.decompose_map

added theorem GradedRingHom.cancel_left

added theorem GradedRingHom.cancel_right

added theorem GradedRingHom.coe_comp

added theorem GradedRingHom.coe_copy

added theorem GradedRingHom.coe_id

added theorem GradedRingHom.coe_inj

added theorem GradedRingHom.coe_mk

added theorem GradedRingHom.coe_mul

added theorem GradedRingHom.coe_ofClass

added theorem GradedRingHom.coe_one

added theorem GradedRingHom.coe_pow

added theorem GradedRingHom.coe_ringHom_injective

added theorem GradedRingHom.coe_toRingHom

added def GradedRingHom.comp

added theorem GradedRingHom.comp_apply

added theorem GradedRingHom.comp_assoc

added theorem GradedRingHom.comp_id

added def GradedRingHom.copy

added theorem GradedRingHom.copy_eq

added theorem GradedRingHom.ext

added def GradedRingHom.gradedAddHom

added def GradedRingHom.gradedZeroRingHom

added def GradedRingHom.id

added theorem GradedRingHom.id_apply

added theorem GradedRingHom.id_comp

added theorem GradedRingHom.map_directSumDecompose

added theorem GradedRingHom.mk_coe

added theorem GradedRingHom.mul_def

added def GradedRingHom.ofClass

added theorem GradedRingHom.one_def

added theorem GradedRingHom.toRingHom_eq_toRingHom

added theorem GradedRingHom.toRingHom_id

added structure GradedRingHom

added theorem map_directSumDecompose