English
A helper to build a GradedAlgebra when an underlying SetLike.GradedMonoid structure is given via a decompose map, ensuring right-inverse and left-inverse properties.
Русский
Помощь по конструированию GradedAlgebra из заданной структуры SetLike.GradedMonoid через отображение разложения, обеспечивая правую и левую обращения.
LaTeX
$$$\text{ofAlgHom}[\text{SetLike.GradedMonoid } 𝒜] (decompose : A \to ⨁ i, 𝒜 i) (\text{right_inv} : (DirectSum.coeAlgHom 𝒜) \circ decompose = AlgHom.id) (\text{left_inv} : ∀ i x, decompose x = DirectSum.of (⋯) i x) : GradedAlgebra 𝒜.$$$
Lean4
/-- A helper to construct a `GradedAlgebra` when the `SetLike.GradedMonoid` structure is already
available. This makes the `left_inv` condition easier to prove, and phrases the `right_inv`
condition in a way that allows custom `@[ext]` lemmas to apply.
See note [reducible non-instances]. -/
abbrev ofAlgHom [SetLike.GradedMonoid 𝒜] (decompose : A →ₐ[R] ⨁ i, 𝒜 i)
(right_inv : (DirectSum.coeAlgHom 𝒜).comp decompose = AlgHom.id R A)
(left_inv : ∀ i (x : 𝒜 i), decompose (x : A) = DirectSum.of (fun i => ↥(𝒜 i)) i x) : GradedAlgebra 𝒜
where
decompose' := decompose
left_inv := AlgHom.congr_fun right_inv
right_inv := by
suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this
ext i x : 2
exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)
