Commit 2025-12-14 12:40 3ac4753d

View on Github →

feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes (#26719) The definition of polynomial laws restricts its operations to a fixed universe. This PR constructs the extension to any universe. This is part of the project of studying divided powers on rings, in particular, for studying the universal divided power algebra of a module.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

added theorem AlgHom.val_comp_rangeRestrict

added theorem Subalgebra.val_comp_inclusion

Modified Mathlib/RingTheory/Congruence/Hom.lean

added theorem RingCon.quotientKerEquivRangeₐ_comp_mkₐ

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

added theorem PolynomialLaw.exists_lift'

added theorem PolynomialLaw.exists_lift

added theorem PolynomialLaw.exists_lift_of_mem_range_rTensor

added theorem PolynomialLaw.exists_range_φ_eq_of_fg

added theorem PolynomialLaw.factorsThrough_toFunLifted_π

added theorem PolynomialLaw.isCompat

added theorem PolynomialLaw.isCompat_apply

added def PolynomialLaw.lifts

added theorem PolynomialLaw.one_tmul_ground

added theorem PolynomialLaw.range_φ

added theorem PolynomialLaw.toFun'_eq_of_diagram

added theorem PolynomialLaw.toFun'_eq_of_inclusion

added theorem PolynomialLaw.toFun'_eq_toFun

added def PolynomialLaw.toFun

added def PolynomialLaw.toFunLifted

added theorem PolynomialLaw.toFun_add

added theorem PolynomialLaw.toFun_add_apply

added theorem PolynomialLaw.toFun_comp

added theorem PolynomialLaw.toFun_comp_apply

added theorem PolynomialLaw.toFun_eq_rTensor_φ_toFun'

added theorem PolynomialLaw.toFun_neg

added theorem PolynomialLaw.toFun_smul

added theorem PolynomialLaw.toFun_zero

added def PolynomialLaw.π

added theorem PolynomialLaw.π_surjective

added def PolynomialLaw.φ