feat(algebra/lie/{submodule,subalgebra}): lie_span, coe form a Ga…

…lois insertion (#8213)

src/algebra/lie/subalgebra.lean

@@ -456,6 +456,29 @@ begin
   { rw [← coe_to_submodule_mk p h, coe_to_submodule, coe_to_submodule_eq_iff, lie_span_eq], },
 end
 
+variables (R L)
+
+/-- `lie_span` forms a Galois insertion with the coercion from `lie_subalgebra` to `set`. -/
+protected def gi : galois_insertion (lie_span R L : set L → lie_subalgebra R L) coe :=
+{ choice    := λ s _, lie_span R L s,
+  gc        := λ s t, lie_span_le,
+  le_l_u    := λ s, subset_lie_span,
+  choice_eq := λ s h, rfl }
+
+@[simp] lemma span_empty : lie_span R L (∅ : set L) = ⊥ :=
+(lie_subalgebra.gi R L).gc.l_bot
+
+@[simp] lemma span_univ : lie_span R L (set.univ : set L) = ⊤ :=
+eq_top_iff.2 $ set_like.le_def.2 $ subset_lie_span
+
+variables {L}
+
+lemma span_union (s t : set L) : lie_span R L (s ∪ t) = lie_span R L s ⊔ lie_span R L t :=
+(lie_subalgebra.gi R L).gc.l_sup
+
+lemma span_Union {ι} (s : ι → set L) : lie_span R L (⋃ i, s i) = ⨆ i, lie_span R L (s i) :=
+(lie_subalgebra.gi R L).gc.l_supr
+
 end lie_span
 
 end lie_subalgebra

src/algebra/lie/submodule.lean

@@ -431,6 +431,29 @@ begin
   { rw [← coe_to_submodule_mk p h, coe_to_submodule, coe_to_submodule_eq_iff, lie_span_eq], },
 end
 
+variables (R L M)
+
+/-- `lie_span` forms a Galois insertion with the coercion from `lie_submodule` to `set`. -/
+protected def gi : galois_insertion (lie_span R L : set M → lie_submodule R L M) coe :=
+{ choice    := λ s _, lie_span R L s,
+  gc        := λ s t, lie_span_le,
+  le_l_u    := λ s, subset_lie_span,
+  choice_eq := λ s h, rfl }
+
+@[simp] lemma span_empty : lie_span R L (∅ : set M) = ⊥ :=
+(lie_submodule.gi R L M).gc.l_bot
+
+@[simp] lemma span_univ : lie_span R L (set.univ : set M) = ⊤ :=
+eq_top_iff.2 $ set_like.le_def.2 $ subset_lie_span
+
+variables {M}
+
+lemma span_union (s t : set M) : lie_span R L (s ∪ t) = lie_span R L s ⊔ lie_span R L t :=
+(lie_submodule.gi R L M).gc.l_sup
+
+lemma span_Union {ι} (s : ι → set M) : lie_span R L (⋃ i, s i) = ⨆ i, lie_span R L (s i) :=
+(lie_submodule.gi R L M).gc.l_supr
+
 end lie_span
 
 end lattice_structure