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) : Basis ι R Hᵐᵒᵖ

The multiplicative opposite of a basis: b.mulOpposite i ↦ op (b i).

Equations

• b.mulOpposite = b.map (MulOpposite.opLinearEquiv R)

@[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] : 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