diff --git a/src/algebra/lie/abelian.lean b/src/algebra/lie/abelian.lean index b129694f4075a..b02e077d53e5f 100644 --- a/src/algebra/lie/abelian.lean +++ b/src/algebra/lie/abelian.lean @@ -53,7 +53,7 @@ lemma function.injective.is_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Typ {f : L₁ →ₗ⁅R⁆ L₂} (h₁ : function.injective f) (h₂ : is_lie_abelian L₂) : is_lie_abelian L₁ := { trivial := λ x y, - by { apply h₁, rw [lie_algebra.map_lie, trivial_lie_zero, lie_algebra.map_zero], } } + by { apply h₁, rw [lie_hom.map_lie, trivial_lie_zero, lie_hom.map_zero], } } lemma function.surjective.is_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] @@ -63,7 +63,7 @@ lemma function.surjective.is_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Ty begin obtain ⟨u, hu⟩ := h₁ x, rw ← hu, obtain ⟨v, hv⟩ := h₁ y, rw ← hv, - rw [← lie_algebra.map_lie, trivial_lie_zero, lie_algebra.map_zero], + rw [← lie_hom.map_lie, trivial_lie_zero, lie_hom.map_zero], end } lemma lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} @@ -101,7 +101,7 @@ protected def ker : lie_ideal R L := (to_endomorphism R L M).ker @[simp] protected lemma mem_ker (x : L) : x ∈ lie_module.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0 := begin dunfold lie_module.ker, - simp only [lie_algebra.morphism.mem_ker, linear_map.ext_iff, linear_map.zero_apply, + simp only [lie_hom.mem_ker, linear_map.ext_iff, linear_map.zero_apply, to_endomorphism_apply_apply], end diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean index d0d762687f7e6..039b473dfc8d7 100644 --- a/src/algebra/lie/basic.lean +++ b/src/algebra/lie/basic.lean @@ -19,8 +19,8 @@ modules, morphisms and equivalences, as well as various lemmas to make these def * `lie_algebra` * `lie_ring_module` * `lie_module` - * `lie_algebra.morphism` - * `lie_algebra.equiv` + * `lie_hom` + * `lie_equiv` * `lie_module_hom` * `lie_module_equiv` @@ -133,31 +133,29 @@ by { rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie] end basic_properties -namespace lie_algebra - set_option old_structure_cmd true /-- A morphism of Lie algebras is a linear map respecting the bracket operations. -/ -structure morphism (R : Type u) (L : Type v) (L' : Type w) +structure lie_hom (R : Type u) (L : Type v) (L' : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] - extends linear_map R L L' := -(map_lie : ∀ {x y : L}, to_fun ⁅x, y⁆ = ⁅to_fun x, to_fun y⁆) + extends L →ₗ[R] L' := +(map_lie' : ∀ {x y : L}, to_fun ⁅x, y⁆ = ⁅to_fun x, to_fun y⁆) -attribute [nolint doc_blame] lie_algebra.morphism.to_linear_map +attribute [nolint doc_blame] lie_hom.to_linear_map -notation L ` →ₗ⁅`:25 R:25 `⁆ `:0 L':0 := morphism R L L' +notation L ` →ₗ⁅`:25 R:25 `⁆ `:0 L':0 := lie_hom R L L' -section morphism_properties +namespace lie_hom variables {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] variables [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] -instance : has_coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) := ⟨morphism.to_linear_map⟩ +instance : has_coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) := ⟨lie_hom.to_linear_map⟩ /-- see Note [function coercion] -/ -instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) := ⟨_, morphism.to_fun⟩ +instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) := ⟨_, lie_hom.to_fun⟩ -initialize_simps_projections lie_algebra.morphism (to_fun → apply) +initialize_simps_projections lie_hom (to_fun → apply) @[simp] lemma coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) : ((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f := rfl @@ -165,75 +163,75 @@ initialize_simps_projections lie_algebra.morphism (to_fun → apply) @[simp, norm_cast] lemma coe_to_linear_map (f : L₁ →ₗ⁅R⁆ L₂) : ((f : L₁ →ₗ[R] L₂) : L₁ → L₂) = f := rfl -@[simp] lemma morphism.map_smul (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) : f (c • x) = c • f x := +@[simp] lemma map_smul (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) : f (c • x) = c • f x := linear_map.map_smul (f : L₁ →ₗ[R] L₂) c x -@[simp] lemma morphism.map_add (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x + y) = (f x) + (f y) := +@[simp] lemma map_add (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x + y) = (f x) + (f y) := linear_map.map_add (f : L₁ →ₗ[R] L₂) x y -@[simp] lemma map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ := morphism.map_lie f +@[simp] lemma map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ := lie_hom.map_lie' f @[simp] lemma map_zero (f : L₁ →ₗ⁅R⁆ L₂) : f 0 = 0 := (f : L₁ →ₗ[R] L₂).map_zero /-- The constant 0 map is a Lie algebra morphism. -/ -instance : has_zero (L₁ →ₗ⁅R⁆ L₂) := ⟨{ map_lie := by simp, ..(0 : L₁ →ₗ[R] L₂)}⟩ +instance : has_zero (L₁ →ₗ⁅R⁆ L₂) := ⟨{ map_lie' := by simp, ..(0 : L₁ →ₗ[R] L₂)}⟩ /-- The identity map is a Lie algebra morphism. -/ -instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨{ map_lie := by simp, ..(1 : L₁ →ₗ[R] L₁)}⟩ +instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨{ map_lie' := by simp, ..(1 : L₁ →ₗ[R] L₁)}⟩ instance : inhabited (L₁ →ₗ⁅R⁆ L₂) := ⟨0⟩ -lemma morphism.coe_injective : function.injective (λ f : L₁ →ₗ⁅R⁆ L₂, show L₁ → L₂, from f) := +lemma coe_injective : function.injective (λ f : L₁ →ₗ⁅R⁆ L₂, show L₁ → L₂, from f) := by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr -@[ext] lemma morphism.ext {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g := -morphism.coe_injective $ funext h +@[ext] lemma ext {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g := +coe_injective $ funext h -lemma morphism.ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x := -⟨by { rintro rfl x, refl }, morphism.ext⟩ +lemma ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x := +⟨by { rintro rfl x, refl }, ext⟩ /-- The composition of morphisms is a morphism. -/ -def morphism.comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃ := -{ map_lie := λ x y, by { change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆, rw [map_lie, map_lie], }, +def comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃ := +{ map_lie' := λ x y, by { change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆, rw [map_lie, map_lie], }, ..linear_map.comp f.to_linear_map g.to_linear_map } -@[simp] lemma morphism.comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : +@[simp] lemma comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f.comp g x = f (g x) := rfl @[norm_cast] -lemma morphism.comp_coe (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : +lemma comp_coe (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : (f : L₂ → L₃) ∘ (g : L₁ → L₂) = f.comp g := rfl /-- The inverse of a bijective morphism is a morphism. -/ -def morphism.inverse (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) +def inverse (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : L₂ →ₗ⁅R⁆ L₁ := -{ map_lie := λ x y, +{ map_lie' := λ x y, calc g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ : by { conv_lhs { rw [←h₂ x, ←h₂ y], }, } ... = g (f ⁅g x, g y⁆) : by rw map_lie ... = ⁅g x, g y⁆ : (h₁ _), ..linear_map.inverse f.to_linear_map g h₁ h₂ } -end morphism_properties +end lie_hom /-- An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is more convenient to define via linear equivalence to get `.to_linear_equiv` for free. -/ -structure equiv (R : Type u) (L : Type v) (L' : Type w) +structure lie_equiv (R : Type u) (L : Type v) (L' : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] extends L →ₗ⁅R⁆ L', L ≃ₗ[R] L' -attribute [nolint doc_blame] lie_algebra.equiv.to_morphism -attribute [nolint doc_blame] lie_algebra.equiv.to_linear_equiv +attribute [nolint doc_blame] lie_equiv.to_lie_hom +attribute [nolint doc_blame] lie_equiv.to_linear_equiv -notation L ` ≃ₗ⁅`:50 R `⁆ ` L' := equiv R L L' +notation L ` ≃ₗ⁅`:50 R `⁆ ` L' := lie_equiv R L L' -namespace equiv +namespace lie_equiv variables {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃] variables [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃] -instance has_coe_to_lie_hom : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂) := ⟨to_morphism⟩ +instance has_coe_to_lie_hom : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂) := ⟨to_lie_hom⟩ instance has_coe_to_linear_equiv : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂) := ⟨to_linear_equiv⟩ /-- see Note [function coercion] -/ @@ -246,7 +244,7 @@ instance : has_coe_to_fun (L₁ ≃ₗ⁅R⁆ L₂) := ⟨_, to_fun⟩ ((e : L₁ ≃ₗ[R] L₂) : L₁ → L₂) = e := rfl instance : has_one (L₁ ≃ₗ⁅R⁆ L₁) := -⟨{ map_lie := λ x y, +⟨{ map_lie' := λ x y, by { change ((1 : L₁→ₗ[R] L₁) ⁅x, y⁆) = ⁅(1 : L₁→ₗ[R] L₁) x, (1 : L₁→ₗ[R] L₁) y⁆, simp, }, ..(1 : L₁ ≃ₗ[R] L₁)}⟩ @@ -263,7 +261,7 @@ def refl : L₁ ≃ₗ⁅R⁆ L₁ := 1 /-- Lie algebra equivalences are symmetric. -/ @[symm] def symm (e : L₁ ≃ₗ⁅R⁆ L₂) : L₂ ≃ₗ⁅R⁆ L₁ := -{ ..morphism.inverse e.to_morphism e.inv_fun e.left_inv e.right_inv, +{ ..lie_hom.inverse e.to_lie_hom e.inv_fun e.left_inv e.right_inv, ..e.to_linear_equiv.symm } @[simp] lemma symm_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.symm = e := @@ -278,7 +276,7 @@ by { cases e, refl, } /-- Lie algebra equivalences are transitive. -/ @[trans] def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃ := -{ ..morphism.comp e₂.to_morphism e₁.to_morphism, +{ ..lie_hom.comp e₂.to_lie_hom e₁.to_lie_hom, ..linear_equiv.trans e₁.to_linear_equiv e₂.to_linear_equiv } @[simp] lemma trans_apply (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) : @@ -296,9 +294,7 @@ e.to_linear_equiv.injective lemma surjective (e : L₁ ≃ₗ⁅R⁆ L₂) : function.surjective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) := e.to_linear_equiv.surjective -end equiv - -end lie_algebra +end lie_equiv section lie_module_morphisms @@ -314,7 +310,7 @@ set_option old_structure_cmd true /-- A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra. -/ structure lie_module_hom extends M →ₗ[R] N := -(map_lie : ∀ {x : L} {m : M}, to_fun ⁅x, m⁆ = ⁅x, to_fun m⁆) +(map_lie' : ∀ {x : L} {m : M}, to_fun ⁅x, m⁆ = ⁅x, to_fun m⁆) attribute [nolint doc_blame] lie_module_hom.to_linear_map @@ -335,14 +331,14 @@ instance : has_coe_to_fun (M →ₗ⁅R,L⁆ N) := ⟨_, lie_module_hom.to_fun @[simp, norm_cast] lemma coe_to_linear_map (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f := rfl -@[simp] lemma map_lie' (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ := -lie_module_hom.map_lie f +@[simp] lemma map_lie (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ := +lie_module_hom.map_lie' f /-- The constant 0 map is a Lie module morphism. -/ -instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie := by simp, ..(0 : M →ₗ[R] N) }⟩ +instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M →ₗ[R] N) }⟩ /-- The identity map is a Lie module morphism. -/ -instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie := by simp, ..(1 : M →ₗ[R] M) }⟩ +instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie' := by simp, ..(1 : M →ₗ[R] M) }⟩ instance : inhabited (M →ₗ⁅R,L⁆ N) := ⟨0⟩ @@ -357,7 +353,7 @@ lemma ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m := /-- The composition of Lie module morphisms is a morphism. -/ def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ P := -{ map_lie := λ x m, by { change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆, rw [map_lie', map_lie'], }, +{ map_lie' := λ x m, by { change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆, rw [map_lie, map_lie], }, ..linear_map.comp f.to_linear_map g.to_linear_map } @[simp] lemma comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) : @@ -369,9 +365,9 @@ def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ /-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/ def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : N →ₗ⁅R,L⁆ M := -{ map_lie := λ x n, +{ map_lie' := λ x n, calc g ⁅x, n⁆ = g ⁅x, f (g n)⁆ : by rw h₂ - ... = g (f ⁅x, g n⁆) : by rw map_lie' + ... = g (f ⁅x, g n⁆) : by rw map_lie ... = ⁅x, g n⁆ : (h₁ _), ..linear_map.inverse f.to_linear_map g h₁ h₂ } @@ -402,7 +398,7 @@ instance : has_coe_to_fun (M ≃ₗ⁅R,L⁆ N) := ⟨_, to_fun⟩ @[simp, norm_cast] lemma coe_to_linear_equiv (e : M ≃ₗ⁅R,L⁆ N) : ((e : M ≃ₗ[R] N) : M → N) = e := rfl -instance : has_one (M ≃ₗ⁅R,L⁆ M) := ⟨{ map_lie := λ x m, rfl, ..(1 : M ≃ₗ[R] M) }⟩ +instance : has_one (M ≃ₗ⁅R,L⁆ M) := ⟨{ map_lie' := λ x m, rfl, ..(1 : M ≃ₗ[R] M) }⟩ @[simp] lemma one_apply (m : M) : (1 : (M ≃ₗ⁅R,L⁆ M)) m = m := rfl diff --git a/src/algebra/lie/classical.lean b/src/algebra/lie/classical.lean index debbb64bbec62..f7b763f3e0a29 100644 --- a/src/algebra/lie/classical.lean +++ b/src/algebra/lie/classical.lean @@ -207,14 +207,14 @@ noncomputable def so_indefinite_equiv {i : R} (hi : i*i = -1) : so' p q R ≃ₗ begin apply (skew_adjoint_matrices_lie_subalgebra_equiv (indefinite_diagonal p q R) (Pso p q R i) (is_unit_Pso p q R hi)).trans, - apply lie_algebra.equiv.of_eq, + apply lie_equiv.of_eq, ext A, rw indefinite_diagonal_transform p q R hi, refl, end lemma so_indefinite_equiv_apply {i : R} (hi : i*i = -1) (A : so' p q R) : (so_indefinite_equiv p q R hi A : matrix (p ⊕ q) (p ⊕ q) R) = (Pso p q R i)⁻¹ ⬝ (A : matrix (p ⊕ q) (p ⊕ q) R) ⬝ (Pso p q R i) := -by erw [lie_algebra.equiv.trans_apply, lie_algebra.equiv.of_eq_apply, +by erw [lie_equiv.trans_apply, lie_equiv.of_eq_apply, skew_adjoint_matrices_lie_subalgebra_equiv_apply] /-- A matrix defining a canonical even-rank symmetric bilinear form. @@ -278,7 +278,7 @@ noncomputable def type_D_equiv_so' [invertible (2 : R)] : type_D l R ≃ₗ⁅R⁆ so' l l R := begin apply (skew_adjoint_matrices_lie_subalgebra_equiv (JD l R) (PD l R) (is_unit_PD l R)).trans, - apply lie_algebra.equiv.of_eq, + apply lie_equiv.of_eq, ext A, rw [JD_transform, ← unit_of_invertible_val (2 : R), lie_subalgebra.mem_coe, mem_skew_adjoint_matrices_lie_subalgebra_unit_smul], @@ -359,7 +359,7 @@ begin apply (skew_adjoint_matrices_lie_subalgebra_equiv_transpose (indefinite_diagonal (unit ⊕ l) l R) (matrix.reindex_alg_equiv (equiv.sum_assoc punit l l)) (matrix.reindex_transpose _ _)).trans, - apply lie_algebra.equiv.of_eq, + apply lie_equiv.of_eq, ext A, rw [JB_transform, ← unit_of_invertible_val (2 : R), lie_subalgebra.mem_coe, lie_subalgebra.mem_coe, mem_skew_adjoint_matrices_lie_subalgebra_unit_smul], diff --git a/src/algebra/lie/direct_sum.lean b/src/algebra/lie/direct_sum.lean index 10b0a6b43664a..7e0c8e912fa05 100644 --- a/src/algebra/lie/direct_sum.lean +++ b/src/algebra/lie/direct_sum.lean @@ -52,7 +52,7 @@ variables (R ι L M) /-- The inclusion of each component into a direct sum as a morphism of Lie modules. -/ def lie_module_of [decidable_eq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i := -{ map_lie := λ x m, +{ map_lie' := λ x m, begin ext i, by_cases h : j = i, { rw ← h, simp, }, @@ -62,7 +62,7 @@ def lie_module_of [decidable_eq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i := /-- The projection map onto one component, as a morphism of Lie modules. -/ def lie_module_component (j : ι) : (⨁ i, M i) →ₗ⁅R,L⁆ M j := -{ map_lie := λ x m, +{ map_lie' := λ x m, by simp only [component, lapply_apply, lie_module_bracket_apply, linear_map.to_fun_eq_coe], ..component R ι M j } @@ -96,7 +96,7 @@ 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 +{ map_lie' := λ x y, by { ext i, by_cases h : j = i, { rw ← h, simp, }, { simp [lof, single_eq_of_ne h], }, }, @@ -104,7 +104,8 @@ def lie_algebra_of [decidable_eq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i := /-- 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, by simp only [component, bracket_apply, lapply_apply, linear_map.to_fun_eq_coe], +{ map_lie' := λ x y, + by simp only [component, bracket_apply, lapply_apply, linear_map.to_fun_eq_coe], ..component R ι L j } end algebras diff --git a/src/algebra/lie/ideal_operations.lean b/src/algebra/lie/ideal_operations.lean index ad397177ca2d9..f67eff6181582 100644 --- a/src/algebra/lie/ideal_operations.lean +++ b/src/algebra/lie/ideal_operations.lean @@ -167,7 +167,7 @@ begin let fy₁ : ↥(map f I₁) := ⟨f y₁, mem_map hy₁⟩, let fy₂ : ↥(map f I₂) := ⟨f y₂, mem_map hy₂⟩, change _ ∈ comap f ⁅map f I₁, map f I₂⁆, - simp only [submodule.coe_mk, mem_comap, map_lie], + simp only [submodule.coe_mk, mem_comap, lie_hom.map_lie], exact lie_submodule.lie_mem_lie _ _ fy₁ fy₂, end @@ -189,20 +189,20 @@ begin lie_submodule.sup_coe_to_submodule, f.ker_coe_submodule, ← linear_map.comap_map_eq, lie_submodule.lie_ideal_oper_eq_linear_span, lie_submodule.lie_ideal_oper_eq_linear_span, submodule.map_span], - congr, simp only [coe_to_linear_map, set.mem_set_of_eq], ext y, + congr, simp only [lie_hom.coe_to_linear_map, set.mem_set_of_eq], ext y, split, { rintros ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩, hy⟩, rw ← hy, erw [lie_submodule.mem_inf, f.mem_ideal_range_iff h] at hx₁ hx₂, obtain ⟨⟨z₁, hz₁⟩, hz₁'⟩ := hx₁, rw ← hz₁ at hz₁', obtain ⟨⟨z₂, hz₂⟩, hz₂'⟩ := hx₂, rw ← hz₂ at hz₂', use [⁅z₁, z₂⁆, ⟨z₁, hz₁'⟩, ⟨z₂, hz₂'⟩, rfl], - simp only [hz₁, hz₂, submodule.coe_mk, map_lie], }, + simp only [hz₁, hz₂, submodule.coe_mk, lie_hom.map_lie], }, { rintros ⟨x, ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩, hx⟩, hy⟩, rw [← hy, ← hx], have hz₁' : f z₁ ∈ f.ideal_range ⊓ J₁, { rw lie_submodule.mem_inf, exact ⟨f.mem_ideal_range, hz₁⟩, }, have hz₂' : f z₂ ∈ f.ideal_range ⊓ J₂, { rw lie_submodule.mem_inf, exact ⟨f.mem_ideal_range, hz₂⟩, }, - use [⟨f z₁, hz₁'⟩, ⟨f z₂, hz₂'⟩], simp only [submodule.coe_mk, map_lie], }, + use [⟨f z₁, hz₁'⟩, ⟨f z₂, hz₂'⟩], simp only [submodule.coe_mk, lie_hom.map_lie], }, end lemma map_comap_bracket_eq {J₁ J₂ : lie_ideal R L'} (h : f.is_ideal_morphism) : diff --git a/src/algebra/lie/matrix.lean b/src/algebra/lie/matrix.lean index 67399dd3f71ee..edec3fbd00ccc 100644 --- a/src/algebra/lie/matrix.lean +++ b/src/algebra/lie/matrix.lean @@ -35,7 +35,7 @@ variables {n : Type w} [decidable_eq n] [fintype n] /-- The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the Lie algebra structures. -/ def lie_equiv_matrix' : module.End R (n → R) ≃ₗ⁅R⁆ matrix n n R := -{ map_lie := λ T S, +{ map_lie' := λ T S, begin let f := @linear_map.to_matrix' R _ n n _ _ _, change f (T.comp S - S.comp T) = (f T) * (f S) - (f S) * (f T), @@ -69,7 +69,7 @@ by simp [linear_equiv.symm_conj_apply, matrix.lie_conj, linear_map.to_matrix'_co types is an equivalence of Lie algebras. -/ def matrix.reindex_lie_equiv {m : Type w₁} [decidable_eq m] [fintype m] (e : n ≃ m) : matrix n n R ≃ₗ⁅R⁆ matrix m m R := -{ map_lie := λ M N, by simp only [lie_ring.of_associative_ring_bracket, matrix.reindex_mul, +{ map_lie' := λ M N, by simp only [lie_ring.of_associative_ring_bracket, matrix.reindex_mul, matrix.mul_eq_mul, linear_equiv.map_sub, linear_equiv.to_fun_apply], ..(matrix.reindex_linear_equiv e e) } diff --git a/src/algebra/lie/of_associative.lean b/src/algebra/lie/of_associative.lean index 64fe617c29fab..2dad95cf42446 100644 --- a/src/algebra/lie/of_associative.lean +++ b/src/algebra/lie/of_associative.lean @@ -79,7 +79,7 @@ instance of_associative_algebra : lie_algebra R A := /-- The map `of_associative_algebra` associating a Lie algebra to an associative algebra is functorial. -/ def of_associative_algebra_hom {B : Type w} [ring B] [algebra R B] (f : A →ₐ[R] B) : A →ₗ⁅R⁆ B := - { map_lie := λ x y, show f ⁅x,y⁆ = ⁅f x,f y⁆, + { map_lie' := λ x y, show f ⁅x,y⁆ = ⁅f x,f y⁆, by simp only [lie_ring.of_associative_ring_bracket, alg_hom.map_sub, alg_hom.map_mul], ..f.to_linear_map, } @@ -111,7 +111,7 @@ variables [lie_ring_module L M] [lie_module R L M] map_smul' := λ t, lie_smul t x, }, map_add' := λ x y, by { ext m, apply add_lie, }, map_smul' := λ t x, by { ext m, apply smul_lie, }, - map_lie := λ x y, by { ext m, apply lie_lie, }, } + map_lie' := λ x y, by { ext m, apply lie_lie, }, } /-- The adjoint action of a Lie algebra on itself. -/ def lie_algebra.ad : L →ₗ⁅R⁆ module.End R L := lie_module.to_endomorphism R L L @@ -139,7 +139,7 @@ variables (e : M₁ ≃ₗ[R] M₂) /-- A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms. -/ def lie_conj : module.End R M₁ ≃ₗ⁅R⁆ module.End R M₂ := -{ map_lie := λ f g, show e.conj ⁅f, g⁆ = ⁅e.conj f, e.conj g⁆, +{ map_lie' := λ f g, show e.conj ⁅f, g⁆ = ⁅e.conj f, e.conj g⁆, by simp only [lie_ring.of_associative_ring_bracket, linear_map.mul_eq_comp, e.conj_comp, linear_equiv.map_sub], ..e.conj } @@ -158,8 +158,8 @@ variables (e : A₁ ≃ₐ[R] A₂) /-- An equivalence of associative algebras is an equivalence of associated Lie algebras. -/ def to_lie_equiv : A₁ ≃ₗ⁅R⁆ A₂ := -{ to_fun := e.to_fun, - map_lie := λ x y, by simp [lie_ring.of_associative_ring_bracket], +{ to_fun := e.to_fun, + map_lie' := λ x y, by simp [lie_ring.of_associative_ring_bracket], ..e.to_linear_equiv } @[simp] lemma to_lie_equiv_apply (x : A₁) : e.to_lie_equiv x = e x := rfl diff --git a/src/algebra/lie/quotient.lean b/src/algebra/lie/quotient.lean index b9d0ddd1ee310..92593b439cf24 100644 --- a/src/algebra/lie/quotient.lean +++ b/src/algebra/lie/quotient.lean @@ -59,7 +59,7 @@ variables (N) /-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`. -/ def action_as_endo_map : L →ₗ⁅R⁆ module.End R N.quotient := -{ map_lie := λ x y, by { ext n, apply quotient.induction_on' n, intros m, +{ map_lie' := λ x y, by { ext n, apply quotient.induction_on' n, intros m, change mk ⁅⁅x, y⁆, m⁆ = mk (⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆), congr, apply lie_lie, }, ..linear_map.comp (submodule.mapq_linear (N : submodule R M) ↑N) lie_submodule_invariant } @@ -73,8 +73,8 @@ instance lie_quotient_lie_ring_module : lie_ring_module L N.quotient := add_lie := λ x y n, by { simp only [linear_map.map_add, linear_map.add_apply], }, lie_add := λ x m n, by { simp only [linear_map.map_add, linear_map.add_apply], }, leibniz_lie := λ x y m, show action_as_endo_map _ _ _ = _, - { simp only [lie_algebra.map_lie, lie_ring.of_associative_ring_bracket, sub_add_cancel, - lie_algebra.coe_to_linear_map, linear_map.mul_app, linear_map.sub_apply], } } + { simp only [lie_hom.map_lie, lie_ring.of_associative_ring_bracket, sub_add_cancel, + lie_hom.coe_to_linear_map, linear_map.mul_app, linear_map.sub_apply], } } /-- The quotient of a Lie module by a Lie submodule, is a Lie module. -/ instance lie_quotient_lie_module : lie_module R L N.quotient := diff --git a/src/algebra/lie/skew_adjoint.lean b/src/algebra/lie/skew_adjoint.lean index f8fefa2447485..9b31a8b5af9a4 100644 --- a/src/algebra/lie/skew_adjoint.lean +++ b/src/algebra/lie/skew_adjoint.lean @@ -60,7 +60,7 @@ endomorphisms. -/ def skew_adjoint_lie_subalgebra_equiv : skew_adjoint_lie_subalgebra (B.comp (↑e : N →ₗ[R] M) ↑e) ≃ₗ⁅R⁆ skew_adjoint_lie_subalgebra B := begin - apply lie_algebra.equiv.of_subalgebras _ _ e.lie_conj, + apply lie_equiv.of_subalgebras _ _ e.lie_conj, ext f, simp only [lie_subalgebra.mem_coe, submodule.mem_map_equiv, lie_subalgebra.mem_map_submodule, coe_coe], @@ -112,7 +112,7 @@ iff.rfl skew-adjoint with respect to a square matrix `J` and those with respect to `PᵀJP`. -/ noncomputable def skew_adjoint_matrices_lie_subalgebra_equiv (P : matrix n n R) (h : is_unit P) : skew_adjoint_matrices_lie_subalgebra J ≃ₗ⁅R⁆ skew_adjoint_matrices_lie_subalgebra (Pᵀ ⬝ J ⬝ P) := -lie_algebra.equiv.of_subalgebras _ _ (P.lie_conj h).symm +lie_equiv.of_subalgebras _ _ (P.lie_conj h).symm begin ext A, suffices : P.lie_conj h A ∈ skew_adjoint_matrices_submodule J ↔ @@ -132,7 +132,7 @@ equivalence of Lie algebras of skew-adjoint matrices. -/ def skew_adjoint_matrices_lie_subalgebra_equiv_transpose {m : Type w} [decidable_eq m] [fintype m] (e : matrix n n R ≃ₐ[R] matrix m m R) (h : ∀ A, (e A)ᵀ = e (Aᵀ)) : skew_adjoint_matrices_lie_subalgebra J ≃ₗ⁅R⁆ skew_adjoint_matrices_lie_subalgebra (e J) := -lie_algebra.equiv.of_subalgebras _ _ e.to_lie_equiv +lie_equiv.of_subalgebras _ _ e.to_lie_equiv begin ext A, suffices : J.is_skew_adjoint (e.symm A) ↔ (e J).is_skew_adjoint A, by simpa [this], diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean index 0b630903ba496..8fc067e3cb19a 100644 --- a/src/algebra/lie/subalgebra.lean +++ b/src/algebra/lie/subalgebra.lean @@ -16,11 +16,11 @@ results. * `lie_subalgebra` * `lie_subalgebra.incl` * `lie_subalgebra.map` - * `lie_algebra.morphism.range` - * `lie_algebra.equiv.of_injective` - * `lie_algebra.equiv.of_eq` - * `lie_algebra.equiv.of_subalgebra` - * `lie_algebra.equiv.of_subalgebras` + * `lie_hom.range` + * `lie_equiv.of_injective` + * `lie_equiv.of_eq` + * `lie_equiv.of_subalgebra` + * `lie_equiv.of_subalgebras` ## Tags @@ -120,21 +120,21 @@ variables (f : L →ₗ⁅R⁆ L₂) /-- The embedding of a Lie subalgebra into the ambient space as a Lie morphism. -/ def lie_subalgebra.incl (L' : lie_subalgebra R L) : L' →ₗ⁅R⁆ L := -{ map_lie := λ x y, by { rw [linear_map.to_fun_eq_coe, submodule.subtype_apply], refl, }, +{ map_lie' := λ x y, by { rw [linear_map.to_fun_eq_coe, submodule.subtype_apply], refl, }, ..L'.to_submodule.subtype } /-- The range of a morphism of Lie algebras is a Lie subalgebra. -/ -def lie_algebra.morphism.range : lie_subalgebra R L₂ := +def lie_hom.range : lie_subalgebra R L₂ := { lie_mem' := λ x y, show x ∈ f.to_linear_map.range → y ∈ f.to_linear_map.range → ⁅x, y⁆ ∈ f.to_linear_map.range, by { repeat { rw linear_map.mem_range }, rintros ⟨x', hx⟩ ⟨y', hy⟩, refine ⟨⁅x', y'⁆, _⟩, - rw [←hx, ←hy], change f ⁅x', y'⁆ = ⁅f x', f y'⁆, rw lie_algebra.map_lie, }, + rw [←hx, ←hy], change f ⁅x', y'⁆ = ⁅f x', f y'⁆, rw lie_hom.map_lie, }, ..f.to_linear_map.range } -@[simp] lemma lie_algebra.morphism.range_bracket (x y : f.range) : +@[simp] lemma lie_hom.range_bracket (x y : f.range) : (↑⁅x, y⁆ : L₂) = ⁅(↑x : L₂), ↑y⁆ := rfl -@[simp] lemma lie_algebra.morphism.range_coe : (f.range : set L₂) = set.range f := +@[simp] lemma lie_hom.range_coe : (f.range : set L₂) = set.range f := linear_map.range_coe ↑f @[simp] lemma lie_subalgebra.range_incl (L' : lie_subalgebra R L) : L'.incl.range = L' := @@ -147,7 +147,7 @@ def lie_subalgebra.map (L' : lie_subalgebra R L) : lie_subalgebra R L₂ := erw submodule.mem_map at hx, rcases hx with ⟨x', hx', hx⟩, rw ←hx, erw submodule.mem_map at hy, rcases hy with ⟨y', hy', hy⟩, rw ←hy, erw submodule.mem_map, - exact ⟨⁅x', y'⁆, L'.lie_mem hx' hy', lie_algebra.map_lie f x' y'⟩, }, + exact ⟨⁅x', y'⁆, L'.lie_mem hx' hy', lie_hom.map_lie f x' y'⟩, }, ..((L' : submodule R L).map (f : L →ₗ[R] L₂))} @[simp] lemma lie_subalgebra.mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (L' : lie_subalgebra R L) (x : L₂) : @@ -156,19 +156,17 @@ iff.rfl end lie_subalgebra -namespace lie_algebra +namespace lie_equiv variables {R : Type u} {L₁ : Type v} {L₂ : Type w} variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] -namespace equiv - /-- An injective Lie algebra morphism is an equivalence onto its range. -/ noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) : L₁ ≃ₗ⁅R⁆ f.range := have h' : (f : L₁ →ₗ[R] L₂).ker = ⊥ := linear_map.ker_eq_bot_of_injective h, -{ map_lie := λ x y, by { apply set_coe.ext, - simp only [linear_equiv.of_injective_apply, lie_algebra.morphism.range_bracket], +{ map_lie' := λ x y, by { apply set_coe.ext, + simp only [linear_equiv.of_injective_apply, lie_hom.range_bracket], apply f.map_lie, }, ..(linear_equiv.of_injective ↑f h')} @@ -179,7 +177,7 @@ variables (L₁' L₁'' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) /-- Lie subalgebras that are equal as sets are equivalent as Lie algebras. -/ def of_eq (h : (L₁' : set L₁) = L₁'') : L₁' ≃ₗ⁅R⁆ L₁'' := -{ map_lie := λ x y, by { apply set_coe.ext, simp, }, +{ map_lie' := λ x y, by { apply set_coe.ext, simp, }, ..(linear_equiv.of_eq ↑L₁' ↑L₁'' (by {ext x, change x ∈ (L₁' : set L₁) ↔ x ∈ (L₁'' : set L₁), rw h, } )) } @@ -191,7 +189,7 @@ variables (e : L₁ ≃ₗ⁅R⁆ L₂) /-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image. -/ def of_subalgebra : L₁'' ≃ₗ⁅R⁆ (L₁''.map e : lie_subalgebra R L₂) := -{ map_lie := λ x y, by { apply set_coe.ext, exact lie_algebra.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, } +{ map_lie' := λ x y, by { apply set_coe.ext, exact lie_hom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, } ..(linear_equiv.of_submodule (e : L₁ ≃ₗ[R] L₂) ↑L₁'') } @[simp] lemma of_subalgebra_apply (x : L₁'') : ↑(e.of_subalgebra _ x) = e x := rfl @@ -199,7 +197,7 @@ def of_subalgebra : L₁'' ≃ₗ⁅R⁆ (L₁''.map e : lie_subalgebra R L₂) /-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image. -/ def of_subalgebras (h : L₁'.map ↑e = L₂') : L₁' ≃ₗ⁅R⁆ L₂' := -{ map_lie := λ x y, by { apply set_coe.ext, exact lie_algebra.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, }, +{ map_lie' := λ x y, by { apply set_coe.ext, exact lie_hom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, }, ..(linear_equiv.of_submodules (e : L₁ ≃ₗ[R] L₂) ↑L₁' ↑L₂' (by { rw ←h, refl, })) } @[simp] lemma of_subalgebras_apply (h : L₁'.map ↑e = L₂') (x : L₁') : @@ -208,6 +206,4 @@ def of_subalgebras (h : L₁'.map ↑e = L₂') : L₁' ≃ₗ⁅R⁆ L₂' := @[simp] lemma of_subalgebras_symm_apply (h : L₁'.map ↑e = L₂') (x : L₂') : ↑((e.of_subalgebras _ _ h).symm x) = e.symm x := rfl -end equiv - -end lie_algebra +end lie_equiv diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean index 899cf182fecc6..2e561f6eefc5e 100644 --- a/src/algebra/lie/submodule.lean +++ b/src/algebra/lie/submodule.lean @@ -282,7 +282,7 @@ section inclusion_maps /-- The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules. -/ def incl : N →ₗ⁅R,L⁆ M := -{ map_lie := λ x m, rfl, +{ map_lie' := λ x m, rfl, ..submodule.subtype (N : submodule R M) } @[simp] lemma incl_apply (m : N) : N.incl m = m := rfl @@ -293,7 +293,7 @@ variables {N N'} (h : N ≤ N') /-- Given two nested Lie submodules `N ⊆ N'`, the inclusion `N ↪ N'` is a morphism of Lie modules.-/ def hom_of_le : N →ₗ⁅R,L⁆ N' := -{ map_lie := λ x m, rfl, +{ map_lie' := λ x m, rfl, ..submodule.of_le h } @[simp] lemma coe_hom_of_le (m : N) : (hom_of_le h m : M) = m := rfl @@ -452,7 +452,7 @@ end end lie_ideal -namespace lie_algebra.morphism +namespace lie_hom variables (f : L →ₗ⁅R⁆ L') (I : lie_ideal R L) (J : lie_ideal R L') @@ -478,7 +478,7 @@ lemma ker_le_comap : f.ker ≤ J.comap f := lie_ideal.comap_mono bot_le @[simp] lemma mem_ker {x : L} : x ∈ ker f ↔ f x = 0 := show x ∈ (f.ker : submodule R L) ↔ _, -by simp only [ker_coe_submodule, linear_map.mem_ker, lie_algebra.coe_to_linear_map] +by simp only [ker_coe_submodule, linear_map.mem_ker, coe_to_linear_map] lemma mem_ideal_range {x : L} : f x ∈ ideal_range f := lie_ideal.mem_map (lie_submodule.mem_top x) @@ -501,9 +501,9 @@ by { rw ← le_bot_iff, exact lie_ideal.map_le_iff_le_comap, } lemma ker_eq_bot : f.ker = ⊥ ↔ function.injective f := by rw [← lie_submodule.coe_to_submodule_eq_iff, ker_coe_submodule, lie_submodule.bot_coe_submodule, - linear_map.ker_eq_bot, lie_algebra.coe_to_linear_map] + linear_map.ker_eq_bot, coe_to_linear_map] -end lie_algebra.morphism +end lie_hom namespace lie_ideal @@ -519,7 +519,7 @@ end /-- Given two nested Lie ideals `I₁ ⊆ I₂`, the inclusion `I₁ ↪ I₂` is a morphism of Lie algebras. -/ def hom_of_le {I₁ I₂ : lie_ideal R L} (h : I₁ ≤ I₂) : I₁ →ₗ⁅R⁆ I₂ := -{ map_lie := λ x y, rfl, +{ map_lie' := λ x y, rfl, ..submodule.of_le h, } @[simp] lemma coe_hom_of_le {I₁ I₂ : lie_ideal R L} (h : I₁ ≤ I₂) (x : I₁) : diff --git a/src/algebra/lie/universal_enveloping.lean b/src/algebra/lie/universal_enveloping.lean index 65c39f89cae53..62f641d15016d 100644 --- a/src/algebra/lie/universal_enveloping.lean +++ b/src/algebra/lie/universal_enveloping.lean @@ -67,7 +67,7 @@ variables {L} /-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra. -/ def ι : L →ₗ⁅R⁆ universal_enveloping_algebra R L := -{ map_lie := λ x y, by +{ map_lie' := λ x y, by { suffices : mk_alg_hom R L (ιₜ ⁅x, y⁆ + (ιₜ y) * (ιₜ x)) = mk_alg_hom R L ((ιₜ x) * (ιₜ y)), { rw alg_hom.map_mul at this, simp [lie_ring.of_associative_ring_bracket, ← this], }, exact ring_quot.mk_alg_hom_rel _ (rel.lie_compat x y), }, @@ -93,7 +93,7 @@ def lift : (L →ₗ⁅R⁆ A) ≃ (universal_enveloping_algebra R L →ₐ[R] A rfl @[simp] lemma ι_comp_lift : (lift R f) ∘ (ι R) = f := -funext $ lie_algebra.morphism.ext_iff.mp $ (lift R).symm_apply_apply f +funext $ lie_hom.ext_iff.mp $ (lift R).symm_apply_apply f @[simp] lemma lift_ι_apply (x : L) : lift R f (ι R x) = f x := by rw [←function.comp_apply (lift R f) (ι R) x, ι_comp_lift]