Commit 2026-03-06 15:35 1bb9634b

feat(RingTheory): two constructions about base change and restriction of graded algebra (#36226) In the below, S is an R-algebra. First construction (𝒜 is a graded R-algebra, ℬ is a graded S-algebra):

/-- A map from the base change of a graded algebra is the same as a map to the scalar restriction.
In category-theoretical terms, this is an adjunction between:
1. `𝒜 ↦ (𝒜 · |>.baseChange S)`, a functor from Graded `R`-Algebra to Graded `S`-Algebra; and:
2. `ℬ ↦ (ℬ · |>.restrictScalars R)`, a functor from Graded `S`-Algebra to Graded `R`-Algebra.
-/
GradedAlgHom.liftEquiv : (𝒜 →ₐᵍ[R] (ℬ · |>.restrictScalars R)) ≃
    ((𝒜 · |>.baseChange S) →ₐᵍ[S] ℬ)

Second construction (𝒜 and ℬ are graded S-algebras):

/-- Restrict the base ring to a "smaller" ring. -/
GradedAlgHom.restrictScalars (f : 𝒜 →ₐᵍ[S] ℬ) :
    (𝒜 · |>.restrictScalars R) →ₐᵍ[R] (ℬ · |>.restrictScalars R)

In categorical terms, the second construction is the functoriality of restriction (S-GAlg ⥤ R-GAlg), and the first construction is the adjunction with base change (R-GAlg ⥤ S-GAlg, by tensor product).