Documentation

Mathlib.Algebra.Module.Shrink

Transfer module and algebra structures from α to Shrink α #

noncomputable instance Shrink.instModule {R : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] :
Equations
noncomputable def Shrink.linearEquiv (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] :

Shrinking α to a smaller universe preserves module structure.

Equations
Instances For
    @[simp]
    theorem Shrink.linearEquiv_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : Shrink.{v, u_2} α) :
    (linearEquiv R α) a✝ = (equivShrink α).symm a✝
    @[simp]
    theorem Shrink.linearEquiv_symm_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : α) :
    @[deprecated Shrink.linearEquiv (since := "2025-07-11")]
    noncomputable def linearEquivShrink (α : Type u_3) (β : Type u_4) [Semiring α] [AddCommMonoid β] [Module α β] [Small.{u_5, u_4} β] :

    A small module is linearly equivalent to its small model.

    Equations
    Instances For