English
A small algebra is algebraically equivalent to its small model: there is an α-algebra equivalence between β and Shrink β when β is small and has an α-algebra structure.
Русский
Малую алгебру можно алгебраически эквивалентно её малой модели: существует алгебраическое эквивалентное отображение между β и Shrink β при условии, что β мала и есть алгебра над α.
LaTeX
$$$\mathrm{algEquivShrink}(\alpha,\beta): β \simeq_{\alpha\text{-Alg}} \mathrm{Shrink}(\beta)$$$
Lean4
/-- A small algebra is algebra equivalent to its small model. -/
@[deprecated Shrink.algEquiv (since := "2025-07-11")]
def algEquivShrink (α β) [CommSemiring α] [Semiring β] [Algebra α β] [Small β] : β ≃ₐ[α] Shrink β :=
((equivShrink β).symm.algEquiv α).symm
