mathlib3 documentation

algebra.star.module

The star operation, bundled as a star-linear equiv #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define star_linear_equiv, which is the star operation bundled as a star-linear map. It is defined on a star algebra A over the base ring R.

This file also provides some lemmas that need algebra.module.basic imported to prove.

TODO #

@[simp]
theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_int_cast_smul {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_inv_nat_cast_smul {R : Type u_1} {M : Type u_2} [division_semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_inv_int_cast_smul {R : Type u_1} {M : Type u_2} [division_ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [division_ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_rat_smul {R : Type u_1} [add_comm_group R] [star_add_monoid R] [module R] (x : R) (n : ) :
@[simp]
@[simp]
theorem star_linear_equiv_apply (R : Type u_1) {A : Type u_2} [comm_semiring R] [star_ring R] [add_comm_monoid A] [star_add_monoid A] [module R A] [star_module R A] (ᾰ : A) :
def star_linear_equiv (R : Type u_1) {A : Type u_2} [comm_semiring R] [star_ring R] [add_comm_monoid A] [star_add_monoid A] [module R A] [star_module R A] :

If A is a module over a commutative R with compatible actions, then star is a semilinear equivalence.

Equations

The self-adjoint elements of a star module, as a submodule.

Equations

The skew-adjoint elements of a star module, as a submodule.

Equations

The self-adjoint part of an element of a star module, as a linear map.

Equations

The skew-adjoint part of an element of a star module, as a linear map.

Equations

The decomposition of elements of a star module into their self- and skew-adjoint parts, as a linear equivalence.

Equations
@[simp]
theorem algebra_map_star_comm {R : Type u_1} {A : Type u_2} [comm_semiring R] [star_ring R] [semiring A] [star_semigroup A] [algebra R A] [star_module R A] (r : R) :