Commit 2020-05-28 07:50 fa371f7b

View on Github →

feat(linear_algebra/bilinear_form): introduce adjoints of linear maps (#2746) We also use this to define the Lie algebra structure on skew-adjoint endomorphisms / matrices. The motivation is to enable us to define the classical Lie algebras.

Estimated changes

Modified src/algebra/classical_lie_algebras.lean

Modified src/algebra/lie_algebra.lean

added theorem bilin_form.is_skew_adjoint_bracket

added def bilin_form.skew_adjoint_lie_subalgebra

added def bilin_form.skew_adjoint_matrices_lie_embedding

added def bilin_form.skew_adjoint_matrices_lie_subalgebra

added def lie_algebra.morphism.range

added def lie_equiv_matrix'

added def lie_subalgebra.incl

modified def matrix.lie_algebra

modified def matrix.lie_ring

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.is_adjoint_pair.add

added theorem bilin_form.is_adjoint_pair.comp

added theorem bilin_form.is_adjoint_pair.eq

added theorem bilin_form.is_adjoint_pair.mul

added theorem bilin_form.is_adjoint_pair.smul

added theorem bilin_form.is_adjoint_pair.sub

added def bilin_form.is_adjoint_pair

added theorem bilin_form.is_adjoint_pair_id

added theorem bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right

added theorem bilin_form.is_adjoint_pair_zero

added def bilin_form.is_pair_self_adjoint

added def bilin_form.is_pair_self_adjoint_submodule

added def bilin_form.is_self_adjoint

added def bilin_form.is_skew_adjoint

added theorem bilin_form.is_skew_adjoint_iff_neg_self_adjoint

added theorem bilin_form.mem_self_adjoint_submodule

added theorem bilin_form.mem_skew_adjoint_submodule

added theorem bilin_form.neg_apply

added def bilin_form.self_adjoint_submodule

added def bilin_form.skew_adjoint_submodule

added def matrix.is_adjoint_pair

added def matrix.is_self_adjoint

added def matrix.is_skew_adjoint

added theorem matrix_is_adjoint_pair_bilin_form

added theorem mem_pair_self_adjoint_matrices_submodule

added def pair_self_adjoint_matrices_linear_embedding

added theorem pair_self_adjoint_matrices_linear_embedding_apply

added theorem pair_self_adjoint_matrices_linear_embedding_injective

added def pair_self_adjoint_matrices_submodule

added def self_adjoint_matrices_submodule

added def skew_adjoint_matrices_submodule

added theorem to_bilin_form_to_matrix

added theorem to_matrix_to_bilin_form

Modified src/linear_algebra/matrix.lean

added theorem matrix.comp_to_matrix_mul

added theorem matrix.to_lin_neg