noncomputable instance
Shrink.instModule
{R : Type u_1}
{α : Type u_2}
[Small.{v, u_2} α]
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
Module R (Shrink.{v, u_2} α)
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
- Shrink.linearEquiv R α = Equiv.linearEquiv R (equivShrink α).symm
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} α)
:
@[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
- linearEquivShrink α β = LinearEquiv.symm (Equiv.linearEquiv α (equivShrink β).symm)