Commit 2025-06-04 20:26 ae690747

View on Github →

feat: range of lifts (#25276) It turns out that the range of most universal properties can be expressed via adjoin. This adds this result for:

CliffordAlgebra
TensorAlgebra
QuaternionBasis
Complex
TrivSqZeroExt
DualNumber It already exists for FreeAlgebra.

Estimated changes

Modified Mathlib/Algebra/DualNumber.lean

added theorem DualNumber.lift_comp_inlHom

added theorem DualNumber.range_inlAlgHom_sup_adjoin_eps

added theorem DualNumber.range_lift

Modified Mathlib/Algebra/QuaternionBasis.lean

added theorem QuaternionAlgebra.Basis.range_liftHom

Modified Mathlib/Algebra/TrivSqZeroExt.lean

added theorem TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr

added theorem TrivSqZeroExt.range_liftAux

Modified Mathlib/Data/Complex/Module.lean

added theorem Complex.adjoin_I

added theorem Complex.range_liftAux

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

added theorem CliffordAlgebra.adjoin_range_ι

added theorem CliffordAlgebra.range_lift

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

added theorem TensorAlgebra.adjoin_range_ι

added theorem TensorAlgebra.range_lift