Commit 2026-03-05 14:29 e9b5e1a0

View on Github →

feat(RingTheory): define R-linear graded algebra homomorphism (#30365) This PR defines R-linear graded algebra homomorphisms, which are R-algebra homomorphisms that preserve the grading. We also provide the basic properties (aka the "API"). Zulip discussion: #mathlib4 > redefine Graded Algebra

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/GradedAlgebra/AlgHom.lean

added theorem GradedAlgHom.cancel_left

added theorem GradedAlgHom.cancel_right

added theorem GradedAlgHom.coe_addMonoidHom_injective

added theorem GradedAlgHom.coe_algHom_injective

added theorem GradedAlgHom.coe_algHom_mk

added theorem GradedAlgHom.coe_comp

added theorem GradedAlgHom.coe_fn_inj

added theorem GradedAlgHom.coe_fn_injective

added theorem GradedAlgHom.coe_id

added theorem GradedAlgHom.coe_linearMap_injective

added theorem GradedAlgHom.coe_mk'

added theorem GradedAlgHom.coe_mk

added theorem GradedAlgHom.coe_mks

added theorem GradedAlgHom.coe_monoidHom_injective

added theorem GradedAlgHom.coe_mul

added theorem GradedAlgHom.coe_ofClass

added theorem GradedAlgHom.coe_one

added theorem GradedAlgHom.coe_pow

added theorem GradedAlgHom.coe_ringHom_injective

added theorem GradedAlgHom.coe_toAlgHom

added theorem GradedAlgHom.commutes

added def GradedAlgHom.comp

added theorem GradedAlgHom.comp_assoc

added theorem GradedAlgHom.comp_id

added theorem GradedAlgHom.comp_ofId

added theorem GradedAlgHom.comp_toAlgHom

added theorem GradedAlgHom.comp_toGradedRingHom

added theorem GradedAlgHom.default_apply

added theorem GradedAlgHom.ext

added theorem GradedAlgHom.id_comp

added theorem GradedAlgHom.id_toAlgHom

added def GradedAlgHom.mk'

added theorem GradedAlgHom.mk_coe

added def GradedAlgHom.ofClass

added theorem GradedAlgHom.toAlgHom_ofClass

added def GradedAlgHom.toEnd

added theorem GradedAlgHom.toGradedRingHom_injective

added theorem GradedAlgHom.toGradedRingHom_ofClass

added structure GradedAlgHom