From c9593dcc5333e7184216f2082401434745b77170 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 22 Jul 2021 07:37:52 +0000 Subject: [PATCH] feat(algebra/lie/direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369) Various other minor improvements. --- src/algebra/lie/direct_sum.lean | 118 ++++++++++++++++++++-- src/linear_algebra/direct_sum_module.lean | 6 ++ 2 files changed, 115 insertions(+), 9 deletions(-) diff --git a/src/algebra/lie/direct_sum.lean b/src/algebra/lie/direct_sum.lean index 7e0c8e912fa05..dcaa7fb32363f 100644 --- a/src/algebra/lie/direct_sum.lean +++ b/src/algebra/lie/direct_sum.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Nash -/ import algebra.lie.basic +import algebra.lie.submodule +import algebra.lie.of_associative import linear_algebra.direct_sum.finsupp /-! @@ -72,10 +74,10 @@ section algebras /-! The direct sum of Lie algebras carries a natural Lie algebra structure. -/ -variables {L : ι → Type w} +variables (L : ι → Type w) variables [Π i, lie_ring (L i)] [Π i, lie_algebra R (L i)] -instance : lie_ring (⨁ i, L i) := +instance lie_ring : lie_ring (⨁ i, L i) := { bracket := zip_with (λ i, λ x y, ⁅x, y⁆) (λ i, lie_zero 0), add_lie := λ x y z, by { ext, simp only [zip_with_apply, add_apply, add_lie], }, lie_add := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_add], }, @@ -87,7 +89,7 @@ instance : lie_ring (⨁ i, L i) := @[simp] lemma bracket_apply (x y : ⨁ i, L i) (i : ι) : ⁅x, y⁆ i = ⁅x i, y i⁆ := zip_with_apply _ _ x y i -instance : lie_algebra R (⨁ i, L i) := +instance lie_algebra : lie_algebra R (⨁ i, L i) := { lie_smul := λ c x y, by { ext, simp only [ zip_with_apply, smul_apply, bracket_apply, lie_smul] }, ..(infer_instance : module R _) } @@ -95,19 +97,117 @@ instance : lie_algebra R (⨁ i, L i) := variables (R ι L) /-- The inclusion of each component into the direct sum as morphism of Lie algebras. -/ -def lie_algebra_of [decidable_eq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i := -{ map_lie' := λ x y, by +@[simps] def lie_algebra_of [decidable_eq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i := +{ to_fun := of L j, + map_lie' := λ x y, by { ext i, by_cases h : j = i, - { rw ← h, simp, }, - { simp [lof, single_eq_of_ne h], }, }, + { rw ← h, simp [of], }, + { simp [of, single_eq_of_ne h], }, }, ..lof R ι L j, } /-- The projection map onto one component, as a morphism of Lie algebras. -/ -def lie_algebra_component (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j := -{ map_lie' := λ x y, +@[simps] def lie_algebra_component (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j := +{ to_fun := component R ι L j, + map_lie' := λ x y, by simp only [component, bracket_apply, lapply_apply, linear_map.to_fun_eq_coe], ..component R ι L j } +@[ext] lemma lie_algebra_ext {x y : ⨁ i, L i} + (h : ∀ i, lie_algebra_component R ι L i x = lie_algebra_component R ι L i y) : x = y := +dfinsupp.ext h + +include R + +lemma lie_of_of_ne [decidable_eq ι] {i j : ι} (hij : j ≠ i) (x : L i) (y : L j) : + ⁅of L i x, of L j y⁆ = 0 := +begin + apply lie_algebra_ext R ι L, intros k, + rw lie_hom.map_lie, + simp only [component, of, lapply_apply, single_add_hom_apply, lie_algebra_component_apply, + single_apply, zero_apply], + by_cases hik : i = k, + { simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij], }, + { simp only [dif_neg, not_false_iff, zero_lie, hik], }, +end + +lemma lie_of_of_eq [decidable_eq ι] {i j : ι} (hij : j = i) (x : L i) (y : L j) : + ⁅of L i x, of L j y⁆ = of L i ⁅x, hij.rec_on y⁆ := +begin + have : of L j y = of L i (hij.rec_on y), { exact eq.drec (eq.refl _) hij, }, + rw [this, ← lie_algebra_of_apply R ι L i ⁅x, hij.rec_on y⁆, lie_hom.map_lie, + lie_algebra_of_apply, lie_algebra_of_apply], +end + +@[simp] lemma lie_of [decidable_eq ι] {i j : ι} (x : L i) (y : L j) : + ⁅of L i x, of L j y⁆ = + if hij : j = i then lie_algebra_of R ι L i ⁅x, hij.rec_on y⁆ else 0 := +begin + by_cases hij : j = i, + { simp only [lie_of_of_eq R ι L hij x y, hij, dif_pos, not_false_iff, lie_algebra_of_apply], }, + { simp only [lie_of_of_ne R ι L hij x y, hij, dif_neg, not_false_iff], }, +end + +variables {R L ι} + +/-- Given a family of Lie algebras `L i`, together with a family of morphisms of Lie algebras +`f i : L i →ₗ⁅R⁆ L'` into a fixed Lie algebra `L'`, we have a natural linear map: +`(⨁ i, L i) →ₗ[R] L'`. If in addition `⁅f i x, f j y⁆ = 0` for any `x ∈ L i` and `y ∈ L j` (`i ≠ j`) +then this map is a morphism of Lie algebras. -/ +@[simps] def to_lie_algebra [decidable_eq ι] (L' : Type w₁) [lie_ring L'] [lie_algebra R L'] + (f : Π i, L i →ₗ⁅R⁆ L') (hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅f i x, f j y⁆ = 0) : + (⨁ i, L i) →ₗ⁅R⁆ L' := +{ to_fun := to_module R ι L' (λ i, (f i : L i →ₗ[R] L')), + map_lie' := λ x y, + begin + let f' := λ i, (f i : L i →ₗ[R] L'), + /- The goal is linear in `y`. We can use this to reduce to the case that `y` has only one + non-zero component. -/ + suffices : ∀ (i : ι) (y : L i), to_module R ι L' f' ⁅x, of L i y⁆ = + ⁅to_module R ι L' f' x, to_module R ι L' f' (of L i y)⁆, + { simp only [← lie_algebra.ad_apply R, ← linear_map.comp_apply], + congr, clear y, ext i y, exact this i y, }, + /- Similarly, we can reduce to the case that `x` has only one non-zero component. -/ + suffices : ∀ i j (y : L i) (x : L j), to_module R ι L' f' ⁅of L j x, of L i y⁆ = + ⁅to_module R ι L' f' (of L j x), to_module R ι L' f' (of L i y)⁆, + { intros i y, + rw [← lie_skew x, ← lie_skew (to_module R ι L' f' x)], + simp only [linear_map.map_neg, neg_inj, ← lie_algebra.ad_apply R, ← linear_map.comp_apply], + congr, clear x, ext j x, exact this j i x y, }, + /- Tidy up and use `lie_of`. -/ + intros i j y x, + simp only [lie_of R, lie_algebra_of_apply, lie_hom.coe_to_linear_map, to_add_monoid_of, + coe_to_module_eq_coe_to_add_monoid, linear_map.to_add_monoid_hom_coe], + /- And finish with trivial case analysis. -/ + rcases eq_or_ne i j with h | h, + { have h' : f j (h.rec_on y) = f i y, { exact eq.drec (eq.refl _) h, }, + simp only [h, h', lie_hom.coe_to_linear_map, dif_pos, lie_hom.map_lie, to_add_monoid_of, + linear_map.to_add_monoid_hom_coe], }, + { simp only [h, hf j i h.symm x y, dif_neg, not_false_iff, add_monoid_hom.map_zero], }, + end, +.. to_module R ι L' (λ i, (f i : L i →ₗ[R] L')) } + end algebras +section ideals + +variables {L : Type w} [lie_ring L] [lie_algebra R L] (I : ι → lie_ideal R L) + +/-- Given a Lie algebra `L` and a family of ideals `I i ⊆ L`, informally this definition is the +statement that `L = ⨁ i, I i`. + +More formally, the inclusions give a natural map from the (external) direct sum to the enclosing Lie +algebra: `(⨁ i, I i) → L`, and this definition is the proposition that this map is bijective. -/ +def lie_algebra_is_internal [decidable_eq ι] : Prop := +function.bijective $ to_module R ι L $ λ i, ((I i).incl : I i →ₗ[R] L) + +/-- The fact that this instance is necessary seems to be a bug in typeclass inference. See +[this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ +Typeclass.20resolution.20under.20binders/near/245151099). -/ +instance lie_ring_of_ideals : lie_ring (⨁ i, I i) := direct_sum.lie_ring (λ i, ↥(I i)) + +/-- See `direct_sum.lie_ring_of_ideals` comment. -/ +instance lie_algebra_of_ideals : lie_algebra R (⨁ i, I i) := direct_sum.lie_algebra (λ i, ↥(I i)) + +end ideals + end direct_sum diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean index dc0e040156d1a..84bcb9777947b 100644 --- a/src/linear_algebra/direct_sum_module.lean +++ b/src/linear_algebra/direct_sum_module.lean @@ -81,6 +81,12 @@ variables (R ι N φ) def to_module : (⨁ i, M i) →ₗ[R] N := dfinsupp.lsum ℕ φ +/-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor +from modules to additive monoids. -/ +lemma coe_to_module_eq_coe_to_add_monoid : + (to_module R ι N φ : (⨁ i, M i) → N) = to_add_monoid (λ i, (φ i).to_add_monoid_hom) := +rfl + variables {ι N φ} /-- The map constructed using the universal property gives back the original maps when