Documentation

Mathlib.Algebra.Algebra.Shrink

Transfer module and algebra structures from α to Shrink α #

source
instance Shrink.instAlgebra {R : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [CommSemiring R] [Semiring α] [Algebra R α] :
Algebra R (Shrink.{v, u_2} α)
Equations
source
def Shrink.algEquiv (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] :
Shrink.{v, u_2} α ≃ₐ[R] α

Shrinking α to a smaller universe preserves algebra structure.

Equations
Instances For
    source
    @[simp]
    theorem Shrink.algEquiv_apply (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] (a✝ : Shrink.{v, u_2} α) :
    (algEquiv R α) a✝ = (equivShrink α).symm a✝
    source
    @[simp]
    theorem Shrink.algEquiv_symm_apply (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] (a✝ : α) :
    (algEquiv R α).symm a✝ = (equivShrink α) a✝
    source
    @[deprecated Shrink.algEquiv (since := "2025-07-11")]
    def algEquivShrink (α : Type u_3) (β : Type u_4) [CommSemiring α] [Semiring β] [Algebra α β] [Small.{u_5, u_4} β] :
    β ≃ₐ[α] Shrink.{u_5, u_4} β

    A small algebra is algebra equivalent to its small model.

    Equations
    Instances For