Commit 2021-01-18 10:20 66e955e4

View on Github →

feat(algebra/lie/basic): results relating Lie algebra morphisms and ideal operations (#5778) The key results are lie_ideal.comap_bracket_eq and its corollary lie_ideal.comap_bracket_incl

Estimated changes

Modified src/algebra/lie/basic.lean

deleted theorem coe_to_subalgebra

added def lie_algebra.morphism.ideal_range

added def lie_algebra.morphism.is_ideal_morphism

added theorem lie_algebra.morphism.is_ideal_morphism_def

added def lie_algebra.morphism.ker

added theorem lie_algebra.morphism.ker_coe_submodule

added theorem lie_algebra.morphism.ker_le_comap

added theorem lie_algebra.morphism.map_le_ideal_range

added theorem lie_algebra.morphism.mem_ideal_range

added theorem lie_algebra.morphism.mem_ideal_range_iff

added theorem lie_algebra.morphism.mem_ker

added theorem lie_algebra.morphism.range_subset_ideal_range

added theorem lie_ideal.coe_to_subalgebra

modified def lie_ideal.comap

added theorem lie_ideal.comap_bracket_eq

added theorem lie_ideal.comap_bracket_incl

added theorem lie_ideal.comap_bracket_incl_of_le

added theorem lie_ideal.comap_bracket_le

added theorem lie_ideal.comap_coe_submodule

added theorem lie_ideal.comap_incl_self

added theorem lie_ideal.comap_map_eq

added theorem lie_ideal.comap_map_le

added theorem lie_ideal.comap_mono

modified theorem lie_ideal.gc_map_comap

modified def lie_ideal.incl

modified theorem lie_ideal.incl_apply

added theorem lie_ideal.incl_coe

added theorem lie_ideal.incl_ideal_range

added theorem lie_ideal.incl_is_ideal_morphism

added theorem lie_ideal.ker_incl

modified def lie_ideal.map

added theorem lie_ideal.map_bracket_le

added theorem lie_ideal.map_coe_submodule

added theorem lie_ideal.map_comap_bracket_eq

added theorem lie_ideal.map_comap_eq

added theorem lie_ideal.map_comap_incl

added theorem lie_ideal.map_comap_le

added theorem lie_ideal.map_le

modified theorem lie_ideal.map_le_iff_le_comap

added theorem lie_ideal.map_mono

added theorem lie_ideal.map_of_image

added theorem lie_ideal.map_sup_ker_eq_map

added theorem lie_ideal.mem_comap

added theorem lie_ideal.mem_map

modified theorem lie_subalgebra.coe_bracket

added theorem lie_subalgebra.coe_set_eq_iff

added theorem lie_subalgebra.coe_to_set_mk

added theorem lie_subalgebra.coe_to_submodule_eq_iff

modified theorem lie_subalgebra.ext

modified theorem lie_subalgebra.ext_iff

modified theorem lie_subalgebra.mem_coe'

modified theorem lie_subalgebra.mem_coe

added theorem lie_subalgebra.range_incl