refactor(RingTheory/HopfAlgebra/Generators): LinearMap namespace, right-handed twins

Author: hawkrobe

Mathlib/RingTheory/Bialgebra/Primitive.lean

@@ -23,8 +23,8 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that
 * `primitiveSubmodule` is a `LieSubalgebra` with bracket `[a, b] = a * b - b * a`.
   (`IsPrimitiveElem.commutator` is stated with `a * b - b * a` rather than `⁅a, b⁆` to avoid
   importing Lie theory into this file.)
-* In characteristic 0 over a field, the primitive elements of a cocommutative connected
-  bialgebra generate it as the universal enveloping of a Lie algebra.
+* (Cartier–Milnor–Moore) In characteristic 0 over a field, the primitive elements of a
+  cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra.
 * Generalize to `(g, h)`-skew-primitive elements `Δ a = a ⊗ₜ g + h ⊗ₜ a` for group-like `g`, `h`
   over a plain coalgebra, of which primitivity is the `(1, 1)` case over a bialgebra.
 -/

Mathlib/RingTheory/HopfAlgebra/Generators.lean

@@ -19,33 +19,34 @@ antimultiplicative antipode data on generators.
 
 ## Main results
 
-* `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_left` and
-  `HopfAlgebra.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of
+* `LinearMap.convMul_eq_one_of_adjoin_eq_top_left` and
+  `LinearMap.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of
   a multiplicative map on generators is a global one.
-* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` : a left convolution inverse of `id` is the
+* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` and
+  `HopfAlgebra.eq_antipode_of_id_convMul_eq_one`: a one-sided convolution inverse of `id` is the
   antipode.
-* `HopfAlgebra.eq_antipode_of_adjoin_eq_top` : a left convolution inverse of `id` on a generating
-  set is the antipode.
+* `HopfAlgebra.eq_antipode_of_adjoin_eq_top_left` and
+  `HopfAlgebra.eq_antipode_of_adjoin_eq_top_right`: a one-sided convolution inverse of `id` on a
+  generating set is the antipode.
 -/
 
 public section
 
-namespace HopfAlgebra
-
 open Algebra Coalgebra LinearMap WithConv
 
 variable {R A B : Type*} [CommSemiring R]
 
+namespace LinearMap
+
 section ExtensionPrinciple
 
 /-! ### Extension principle from algebra generators -/
 
 variable [Semiring A] [Bialgebra R A] [Semiring B] [Algebra R B]
   {g f : A →ₗ[R] B} {s : Set A}
 
-/-- If a unital antimultiplicative map `g` and a unital multiplicative map `f` satisfy
-`toConv g * toConv f = 1` pointwise on an algebra-generating set, then they do so globally:
-a left convolution inverse on generators is a left convolution inverse. -/
+/-- If a unital antimultiplicative map `g` is a left convolution inverse of a unital
+multiplicative map `f` pointwise on an algebra-generating set, then `toConv g * toConv f = 1`. -/
 theorem convMul_eq_one_of_adjoin_eq_top_left
     (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x)
     (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y)
@@ -54,7 +55,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_left
     toConv g * toConv f = 1 := by
   ext x; refine adjoin_le
     (S := (eqLocus (toConv g * toConv f).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_)
-    g_convMul_f (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s)
+    g_convMul_f (adjoin_eq_top.ge mem_top)
   · simp [g_one, f_one, TensorProduct.one_def]
   let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
   simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢
@@ -66,8 +67,8 @@ theorem convMul_eq_one_of_adjoin_eq_top_left
         rw [Finset.sum_comm]; simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ha, ← commutes]
         simp_rw [mul_assoc, ← Finset.mul_sum, hb, ← map_mul, ← Bialgebra.counit_mul]
 
-/-- Analogue of `convMul_eq_one_of_adjoin_eq_top_left` for `toConv f * toConv g = 1`:
-a right convolution inverse on generators is a right convolution inverse. -/
+/-- If a unital antimultiplicative map `g` is a right convolution inverse of a unital
+multiplicative map `f` pointwise on an algebra-generating set, then `toConv f * toConv g = 1`. -/
 theorem convMul_eq_one_of_adjoin_eq_top_right
     (g_one : g 1 = 1) (g_mul : ∀ x y, g (x * y) = g y * g x)
     (f_one : f 1 = 1) (f_mul : ∀ x y, f (x * y) = f x * f y)
@@ -76,7 +77,7 @@ theorem convMul_eq_one_of_adjoin_eq_top_right
     toConv f * toConv g = 1 := by
   ext x; refine adjoin_le
     (S := (eqLocus (toConv f * toConv g).ofConv (ofConv 1)).toSubalgebra ?_ fun a b ha hb => ?_)
-    f_convMul_g (adjoin_eq_top ▸ mem_top : x ∈ adjoin R s)
+    f_convMul_g (adjoin_eq_top.ge mem_top)
   · simp [g_one, f_one, TensorProduct.one_def]
   let 𝓡a := ℛ R a; let 𝓡b := ℛ R b
   simp only [mem_eqLocus, 𝓡a.convMul_apply, 𝓡b.convMul_apply, convOne_apply] at ha hb ⊢
@@ -91,6 +92,10 @@ theorem convMul_eq_one_of_adjoin_eq_top_right
 
 end ExtensionPrinciple
 
+end LinearMap
+
+namespace HopfAlgebra
+
 section Construction
 variable [Semiring A] [Bialgebra R A] {S₀ : A →ₗ[R] A} {s : Set A}
 
@@ -121,10 +126,14 @@ theorem eq_antipode_of_convMul_id_eq_one (h : toConv S₀ * toConv LinearMap.id
     S₀ = antipode R :=
   toConv_injective (left_inv_eq_right_inv h id_mul_antipode)
 
-variable (S₀) in
+/-- A right convolution inverse of the identity is the antipode. -/
+theorem eq_antipode_of_id_convMul_eq_one (h : toConv LinearMap.id * toConv S₀ = 1) :
+    S₀ = antipode R :=
+  toConv_injective (left_inv_eq_right_inv antipode_mul_id h).symm
+
 /-- A unital antimultiplicative map that is a left convolution inverse of the identity on an
 algebra-generating set is the antipode. -/
-theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1)
+theorem eq_antipode_of_adjoin_eq_top_left (S₀_one : S₀ 1 = 1)
     (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤)
     (S₀_convMul_id : ∀ p ∈ s,
       (toConv S₀ * toConv (.id : A →ₗ[R] A)) p = (1 : WithConv (A →ₗ[R] A)) p) :
@@ -133,6 +142,17 @@ theorem eq_antipode_of_adjoin_eq_top (S₀_one : S₀ 1 = 1)
     (convMul_eq_one_of_adjoin_eq_top_left S₀_one S₀_mul rfl (fun _ _ => rfl)
       adjoin_eq_top S₀_convMul_id)
 
+/-- A unital antimultiplicative map that is a right convolution inverse of the identity on an
+algebra-generating set is the antipode. -/
+theorem eq_antipode_of_adjoin_eq_top_right (S₀_one : S₀ 1 = 1)
+    (S₀_mul : ∀ x y, S₀ (x * y) = S₀ y * S₀ x) (adjoin_eq_top : adjoin R s = ⊤)
+    (id_convMul_S₀ : ∀ p ∈ s,
+      (toConv (.id : A →ₗ[R] A) * toConv S₀) p = (1 : WithConv (A →ₗ[R] A)) p) :
+    S₀ = antipode R :=
+  eq_antipode_of_id_convMul_eq_one
+    (convMul_eq_one_of_adjoin_eq_top_right S₀_one S₀_mul rfl (fun _ _ => rfl)
+      adjoin_eq_top id_convMul_S₀)
+
 end Uniqueness
 
 end HopfAlgebra

Mathlib/RingTheory/HopfAlgebra/Primitive.lean

@@ -61,8 +61,7 @@ theorem eq_antipode_of_primitives [Ring A] [HopfAlgebra R A] (S : A →ₐ[R] A
     (adjoin_eq_top : Algebra.adjoin R s = ⊤) (prim : ∀ p ∈ s, IsPrimitiveElem R p)
     (S_apply : ∀ p ∈ s, S p = op (-p)) :
     (opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap = antipode R :=
-  eq_antipode_of_adjoin_eq_top ((opLinearEquiv R).symm.toLinearMap ∘ₗ S.toLinearMap)
-    (by simp) (fun _ _ => by simp) adjoin_eq_top
+  eq_antipode_of_adjoin_eq_top_left (by simp) (fun _ _ => by simp) adjoin_eq_top
     (fun p hp => by simp [convMul_apply, prim p hp, S_apply p hp])
 
 end HopfAlgebra