Basis of an opposite space #
This file defines the basis of an opposite space and shows that the opposite space is finite-dimensional and free when the original space is.
noncomputable def
Module.Basis.mulOpposite
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
:
The multiplicative opposite of a basis: b.mulOpposite i ↦ op (b i).
Instances For
@[simp]
theorem
Module.Basis.mulOpposite_apply
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(i : ι)
:
b.mulOpposite i = MulOpposite.op (b i)
theorem
Module.Basis.mulOpposite_repr_eq
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
:
b.mulOpposite.repr = (MulOpposite.opLinearEquiv R).symm ≪≫ₗ b.repr
@[simp]
theorem
Module.Basis.repr_unop_eq_mulOpposite_repr
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(x : Hᵐᵒᵖ)
:
b.repr (MulOpposite.unop x) = b.mulOpposite.repr x
@[simp]
theorem
Module.Basis.mulOpposite_repr_op
{R : Type u_1}
{H : Type u_2}
{ι : Type u_3}
[Semiring R]
[AddCommMonoid H]
[Module R H]
(b : Basis ι R H)
(x : H)
:
b.mulOpposite.repr (MulOpposite.op x) = b.repr x
instance
MulOpposite.instFiniteDimensional
{R : Type u_1}
{H : Type u_2}
[DivisionRing R]
[AddCommGroup H]
[Module R H]
[FiniteDimensional R H]
:
instance
MulOpposite.instFree
{R : Type u_1}
{H : Type u_2}
[Semiring R]
[AddCommMonoid H]
[Module R H]
[Module.Free R H]
:
Module.Free R Hᵐᵒᵖ
theorem
MulOpposite.rank
{R : Type u_1}
{H : Type u_2}
[Semiring R]
[StrongRankCondition R]
[AddCommMonoid H]
[Module R H]
[Module.Free R H]
:
Module.rank R Hᵐᵒᵖ = Module.rank R H
theorem
MulOpposite.finrank
{R : Type u_1}
{H : Type u_2}
[DivisionRing R]
[AddCommGroup H]
[Module R H]
:
Module.finrank R Hᵐᵒᵖ = Module.finrank R H