From 395d8716c3ad03747059d482090e2bb97db612c8 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 1 Jul 2021 18:15:23 +0000 Subject: [PATCH] chore(algebra/lie/free): tidy up after #8153 (#8163) @eric-wieser had some further comments and suggestions which didn't make it into #8153 --- .../free_non_unital_non_assoc_algebra.lean | 12 ++--- src/algebra/lie/free.lean | 49 ++++++++----------- .../lie/non_unital_non_assoc_algebra.lean | 20 ++++++-- 3 files changed, 43 insertions(+), 38 deletions(-) diff --git a/src/algebra/free_non_unital_non_assoc_algebra.lean b/src/algebra/free_non_unital_non_assoc_algebra.lean index fb89548519a69..df7d2a3e79026 100644 --- a/src/algebra/free_non_unital_non_assoc_algebra.lean +++ b/src/algebra/free_non_unital_non_assoc_algebra.lean @@ -63,6 +63,9 @@ instance (R : Type u) [comm_semiring R] : smul_comm_class R (free_non_unital_non_assoc_algebra R X) (free_non_unital_non_assoc_algebra R X) := monoid_algebra.smul_comm_class_self R +instance (R : Type u) [ring R] : add_comm_group (free_non_unital_non_assoc_algebra R X) := +module.add_comm_monoid_to_add_comm_group R + variables {A : Type w} [non_unital_non_assoc_semiring A] variables [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] @@ -93,12 +96,9 @@ by rw [← function.comp_app (lift R f) (of R) x, of_comp_lift] lift R (F ∘ (of R)) = F := by rw [← lift_symm_apply, equiv.apply_symm_apply] -/-- See note [partially-applied ext lemmas]. -/ @[ext] lemma hom_ext {F₁ F₂ : non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A} - (h : F₁ ∘ (of R) = F₂ ∘ (of R)) : F₁ = F₂ := -begin - rw [← lift_symm_apply, ← lift_symm_apply] at h, - exact (lift R).symm.injective h, -end + (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ := +have h' : (lift R).symm F₁ = (lift R).symm F₂, { ext, simp [h], }, +(lift R).symm.injective h' end free_non_unital_non_assoc_algebra diff --git a/src/algebra/lie/free.lean b/src/algebra/lie/free.lean index 8323bb53f7dde..737898190d191 100644 --- a/src/algebra/lie/free.lean +++ b/src/algebra/lie/free.lean @@ -84,6 +84,9 @@ variables {R X} lemma rel.add_left (a b c : lib R X) (h : rel R X b c) : rel R X (a + b) (a + c) := by { rw [add_comm _ b, add_comm _ c], exact rel.add_right _ _ _ h, } +lemma rel.neg (a b : lib R X) (h : rel R X a b) : rel R X (-a) (-b) := +h.smul (-1) _ _ + end free_lie_algebra /-- The free Lie algebra on the type `X` with coefficients in the commutative ring `R`. -/ @@ -92,44 +95,34 @@ def free_lie_algebra := quot (free_lie_algebra.rel R X) namespace free_lie_algebra -instance : has_scalar R (free_lie_algebra R X) := -{ smul := λ t a, quot.lift_on a (λ x, quot.mk _ (t • x)) (λ a b h, quot.sound (rel.smul t a b h)), } - -instance : has_add (free_lie_algebra R X) := -{ add := quot.map₂ (+) rel.add_left rel.add_right, } - instance : add_comm_group (free_lie_algebra R X) := -{ add_comm := by { rintros ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw add_comm, }, +{ add := quot.map₂ (+) rel.add_left rel.add_right, + add_comm := by { rintros ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw add_comm, }, add_assoc := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_assoc, }, zero := quot.mk _ 0, zero_add := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw zero_add, }, add_zero := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw add_zero, }, - neg := λ x, (-1 : R) • x, - sub := λ x y, x + ((-1 : R) • y), - sub_eq_add_neg := λ x y, rfl, - add_left_neg := - by { rintros ⟨a⟩, change quot.mk _ _ = _, erw [neg_smul, one_smul, add_left_neg], refl, }, - ..(infer_instance : has_add _)} - -/-- Note that here we turn the `has_mul` coming from the `non_unital_non_assoc_semiring` structure -on `lib R X` into a `has_bracket` on `free_lie_algebra`. -/ -instance : has_bracket (free_lie_algebra R X) (free_lie_algebra R X) := -{ bracket := quot.map₂ (*) (λ a b c, rel.mul_left a b c) (λ a b c, rel.mul_right a b c), } - -instance : lie_ring (free_lie_algebra R X) := -{ add_lie := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_mul, }, - lie_add := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw mul_add, }, - lie_self := by { rintros ⟨a⟩, exact quot.sound (rel.lie_self a), }, - leibniz_lie := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, exact quot.sound (rel.leibniz_lie a b c), }, } + neg := quot.map has_neg.neg rel.neg, + add_left_neg := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _ , rw add_left_neg, } } instance : module R (free_lie_algebra R X) := -{ one_smul := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw one_smul, }, +{ smul := λ t, quot.map ((•) t) (rel.smul t), + one_smul := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw one_smul, }, mul_smul := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw mul_smul, }, add_smul := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw add_smul, }, smul_add := by { rintros t ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw smul_add, }, zero_smul := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw zero_smul, }, smul_zero := λ t, by { change quot.mk _ _ = quot.mk _ _, rw smul_zero, }, } +/-- Note that here we turn the `has_mul` coming from the `non_unital_non_assoc_semiring` structure +on `lib R X` into a `has_bracket` on `free_lie_algebra`. -/ +instance : lie_ring (free_lie_algebra R X) := +{ bracket := quot.map₂ (*) rel.mul_left rel.mul_right, + add_lie := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_mul, }, + lie_add := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw mul_add, }, + lie_self := by { rintros ⟨a⟩, exact quot.sound (rel.lie_self a), }, + leibniz_lie := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, exact quot.sound (rel.leibniz_lie a b c), }, } + instance : lie_algebra R (free_lie_algebra R X) := { lie_smul := begin @@ -227,9 +220,9 @@ by rw [← function.comp_app (lift R f) (of R) x, of_comp_lift] @[simp] lemma lift_comp_of (F : free_lie_algebra R X →ₗ⁅R⁆ L) : lift R (F ∘ (of R)) = F := by { rw ← lift_symm_apply, exact (lift R).apply_symm_apply F, } -/-- See note [partially-applied ext lemmas]. -/ -@[ext] lemma hom_ext {F₁ F₂ : free_lie_algebra R X →ₗ⁅R⁆ L} (h : F₁ ∘ (of R) = F₂ ∘ (of R)) : +@[ext] lemma hom_ext {F₁ F₂ : free_lie_algebra R X →ₗ⁅R⁆ L} (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ := -by { rw [← lift_symm_apply, ← lift_symm_apply] at h, exact (lift R).symm.injective h, } +have h' : (lift R).symm F₁ = (lift R).symm F₂, { ext, simp [h], }, +(lift R).symm.injective h' end free_lie_algebra diff --git a/src/algebra/lie/non_unital_non_assoc_algebra.lean b/src/algebra/lie/non_unital_non_assoc_algebra.lean index 5cf9828caa805..d9f1769f972f8 100644 --- a/src/algebra/lie/non_unital_non_assoc_algebra.lean +++ b/src/algebra/lie/non_unital_non_assoc_algebra.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2019 Oliver Nash. All rights reserved. +Copyright (c) 2021 Oliver Nash. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Nash -/ @@ -47,21 +47,33 @@ def lie_ring.to_non_unital_non_assoc_semiring : non_unital_non_assoc_semiring L local attribute [instance] lie_ring.to_non_unital_non_assoc_semiring +namespace lie_algebra + /-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can reinterpret the `smul_lie` law as an `is_scalar_tower`. -/ -instance lie_algebra.is_scalar_tower : is_scalar_tower R L L := ⟨smul_lie⟩ +instance is_scalar_tower : is_scalar_tower R L L := ⟨smul_lie⟩ /-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can reinterpret the `lie_smul` law as an `smul_comm_class`. -/ -instance lie_algebra.smul_comm_class : smul_comm_class R L L := ⟨λ t x y, (lie_smul t x y).symm⟩ +instance smul_comm_class : smul_comm_class R L L := ⟨λ t x y, (lie_smul t x y).symm⟩ + +end lie_algebra + +namespace lie_hom variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] /-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can regard a `lie_hom` as a `non_unital_alg_hom`. -/ @[simps] -def lie_hom.to_non_unital_alg_hom (f : L →ₗ⁅R⁆ L₂) : non_unital_alg_hom R L L₂ := +def to_non_unital_alg_hom (f : L →ₗ⁅R⁆ L₂) : non_unital_alg_hom R L L₂ := { to_fun := f, map_zero' := f.map_zero, map_mul' := f.map_lie, ..f } + +lemma to_non_unital_alg_hom_injective : + function.injective (to_non_unital_alg_hom : _ → non_unital_alg_hom R L L₂) := +λ f g h, ext $ non_unital_alg_hom.congr_fun h + +end lie_hom