Skip to content

Commit

Permalink
feat(algebra/lie/basic): define the module and lie_module structu…
Browse files Browse the repository at this point in the history 
…res on morphisms of Lie modules (#7225)

Also sundry `simp` lemmas
  • Loading branch information
@ocfnash
ocfnash committed Apr 17, 2021
1 parent aa44de5 commit 043d046
Showing 1 changed file with 133 additions and 9 deletions.
142 changes: 133 additions & 9 deletions src/algebra/lie/basic.lean
View file
Expand Up @@ -80,9 +80,10 @@ algebra on this module, such that the Lie bracket acts as the commutator of endo

section basic_properties

variables {R : Type u} {L : Type v} {M : Type w}
variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
variables [lie_ring_module L M] [lie_module R L M]
variables {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
variables [comm_ring R] [lie_ring L] [lie_algebra R L]
variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
variables (t : R) (x y z : L) (m n : M)

@[simp] lemma add_lie : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆ := lie_ring_module.add_lie x y m
Expand Down Expand Up @@ -119,6 +120,18 @@ by { rw [←sub_eq_zero, sub_neg_eq_add, ←add_lie], simp, }
@[simp] lemma lie_neg : ⁅x, -m⁆ = -⁅x, m⁆ :=
by { rw [←sub_eq_zero, sub_neg_eq_add, ←lie_add], simp, }

@[simp] lemma sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ :=
by simp [sub_eq_add_neg]

@[simp] lemma lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ :=
by simp [sub_eq_add_neg]

@[simp] lemma nsmul_lie (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆ :=
add_monoid_hom.map_nsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _

@[simp] lemma lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
add_monoid_hom.map_nsmul ⟨λ (m : M), ⁅x, m⁆, lie_zero x, λ _ _, lie_add _ _ _⟩ _ _

@[simp] lemma gsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
add_monoid_hom.map_gsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _

Expand All @@ -131,6 +144,30 @@ by rw [leibniz_lie, add_sub_cancel]
lemma lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 :=
by { rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie], abel, }

instance : lie_ring_module L (M →ₗ[R] N) :=
{ bracket := λ x f,
{ to_fun := λ m, ⁅x, f m⁆ - f ⁅x, m⁆,
map_add' := λ m n, by { simp only [lie_add, linear_map.map_add], abel, },
map_smul' := λ t m, by simp only [smul_sub, linear_map.map_smul, lie_smul], },
add_lie := λ x y f, by
{ ext n, simp only [add_lie, linear_map.coe_mk, linear_map.add_apply, linear_map.map_add],
abel, },
lie_add := λ x f g, by
{ ext n, simp only [linear_map.coe_mk, lie_add, linear_map.add_apply], abel, },
leibniz_lie := λ x y f, by
{ ext n,
simp only [lie_lie, linear_map.coe_mk, linear_map.map_sub, linear_map.add_apply, lie_sub],
abel, }, }

@[simp] lemma bracket_apply (f : M →ₗ[R] N) (x : L) (m : M) : ⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆ := rfl

instance : lie_module R L (M →ₗ[R] N) :=
{ smul_lie := λ t x f, by
{ ext n,
simp only [smul_sub, smul_lie, linear_map.smul_apply, bracket_apply, linear_map.map_smul], },
lie_smul := λ t x f, by
{ ext n, simp only [smul_sub, linear_map.smul_apply, bracket_apply, lie_smul], }, }

end basic_properties

set_option old_structure_cmd true
Expand All @@ -157,9 +194,6 @@ instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) := ⟨_, lie_hom.to_fun⟩

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

@[simp, norm_cast] lemma coe_to_linear_map (f : L₁ →ₗ⁅R⁆ L₂) : ((f : L₁ →ₗ[R] L₂) : L₁ → L₂) = f :=
rfl

Expand All @@ -169,13 +203,23 @@ linear_map.map_smul (f : L₁ →ₗ[R] L₂) c x
@[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_sub (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x - y) = (f x) - (f y) :=
linear_map.map_sub (f : L₁ →ₗ[R] L₂) x y

@[simp] lemma map_neg (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f (-x) = -(f x) :=
linear_map.map_neg (f : L₁ →ₗ[R] L₂) x

@[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₂)}⟩

@[norm_cast, simp] lemma coe_zero : ((0 : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = 0 := rfl

lemma zero_apply (x : L₁) : (0 : L₁ →ₗ⁅R⁆ L₂) x = 0 := rfl

/-- The identity map is a Lie algebra morphism. -/
instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨{ map_lie' := by simp, ..(1 : L₁ →ₗ[R] L₁)}⟩

Expand All @@ -190,6 +234,17 @@ coe_injective $ funext h
lemma ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x :=
⟨by { rintro rfl x, refl }, ext⟩

@[simp] lemma mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) :
(⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f :=
by { ext, refl, }

@[simp] lemma coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) :
((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f := rfl

@[norm_cast, simp] lemma coe_linear_mk (f : L₁ →ₗ[R] L₂) (h₁ h₂ h₃) :
((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ[R] L₂) = ⟨f, h₁, h₂⟩ :=
by { ext, refl, }

/-- The composition of morphisms is a morphism. -/
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], },
Expand Down Expand Up @@ -325,18 +380,34 @@ instance : has_coe (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) := ⟨lie_module_hom.to
/-- see Note [function coercion] -/
instance : has_coe_to_fun (M →ₗ⁅R,L⁆ N) := ⟨_, lie_module_hom.to_fun⟩

@[simp] lemma coe_mk (f : M → N) (h₁ h₂ h₃) :
((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f := rfl

@[simp, norm_cast] lemma coe_to_linear_map (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
rfl

@[simp] lemma map_smul (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) : f (c • x) = c • f x :=
linear_map.map_smul (f : M →ₗ[R] N) c x

@[simp] lemma map_add (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x + y) = (f x) + (f y) :=
linear_map.map_add (f : M →ₗ[R] N) x y

@[simp] lemma map_sub (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x - y) = (f x) - (f y) :=
linear_map.map_sub (f : M →ₗ[R] N) x y

@[simp] lemma map_neg (f : M →ₗ⁅R,L⁆ N) (x : M) : f (-x) = -(f x) :=
linear_map.map_neg (f : M →ₗ[R] N) x

@[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_zero (f : M →ₗ⁅R,L⁆ N) : f 0 = 0 :=
linear_map.map_zero (f : M →ₗ[R] N)

/-- The constant 0 map is a Lie module morphism. -/
instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M →ₗ[R] N) }⟩

@[norm_cast, simp] lemma coe_zero : ((0 : M →ₗ⁅R,L⁆ N) : M → N) = 0 := rfl

lemma zero_apply (m : M) : (0 : M →ₗ⁅R,L⁆ N) m = 0 := rfl

/-- The identity map is a Lie module morphism. -/
instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie' := by simp, ..(1 : M →ₗ[R] M) }⟩

Expand All @@ -351,6 +422,17 @@ coe_injective $ funext h
lemma ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m :=
⟨by { rintro rfl m, refl, }, ext⟩

@[simp] lemma mk_coe (f : M →ₗ⁅R,L⁆ N) (h₁ h₂ h₃) :
(⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) = f :=
by { ext, refl, }

@[simp] lemma coe_mk (f : M → N) (h₁ h₂ h₃) :
((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f := rfl

@[norm_cast, simp] lemma coe_linear_mk (f : M →ₗ[R] N) (h₁ h₂ h₃) :
((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M →ₗ[R] N) = ⟨f, h₁, h₂⟩ :=
by { ext, refl, }

/-- 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], },
Expand All @@ -371,6 +453,48 @@ def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M)
... = ⁅x, g n⁆ : (h₁ _),
..linear_map.inverse f.to_linear_map g h₁ h₂ }

instance : has_add (M →ₗ⁅R,L⁆ N) :=
{ add := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) + (g : M →ₗ[R] N)) }, }

instance : has_sub (M →ₗ⁅R,L⁆ N) :=
{ sub := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) - (g : M →ₗ[R] N)) }, }

instance : has_neg (M →ₗ⁅R,L⁆ N) :=
{ neg := λ f, { map_lie' := by simp, ..(-(f : (M →ₗ[R] N))) }, }

@[norm_cast, simp] lemma coe_add (f g : M →ₗ⁅R,L⁆ N) : ⇑(f + g) = f + g := rfl

lemma add_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f + g) m = f m + g m := rfl

@[norm_cast, simp] lemma coe_sub (f g : M →ₗ⁅R,L⁆ N) : ⇑(f - g) = f - g := rfl

lemma sub_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f - g) m = f m - g m := rfl

@[norm_cast, simp] lemma coe_neg (f : M →ₗ⁅R,L⁆ N) : ⇑(-f) = -f := rfl

lemma neg_apply (f : M →ₗ⁅R,L⁆ N) (m : M) : (-f) m = -(f m) := rfl

instance : add_comm_group (M →ₗ⁅R,L⁆ N) :=
{ zero := 0,
add := (+),
neg := has_neg.neg,
sub := has_sub.sub,
nsmul := λ n f, { map_lie' := λ x m, by simp, ..(n • (f : M →ₗ[R] N)) },
nsmul_zero' := λ f, by { ext, simp, },
nsmul_succ' := λ n f, by { ext, simp [nat.succ_eq_one_add, add_nsmul], },
..(coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub :
add_comm_group (M →ₗ⁅R,L⁆ N)) }

instance : has_scalar R (M →ₗ⁅R,L⁆ N) :=
{ smul := λ t f, { map_lie' := by simp, ..(t • (f : M →ₗ[R] N)) }, }

@[norm_cast, simp] lemma coe_smul (t : R) (f : M →ₗ⁅R,L⁆ N) : ⇑(t • f) = t • f := rfl

lemma smul_apply (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : (t • f) m = t • (f m) := rfl

instance : module R (M →ₗ⁅R,L⁆ N) :=
function.injective.semimodule R ⟨to_fun, rfl, coe_add⟩ coe_injective coe_smul

end lie_module_hom

/-- An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of
Expand Down

0 comments on commit 043d046

Please sign in to comment.