feat(Algebra/QuadraticAlgebra): injectivity and surjectivity of lift (#42439)

Add API for the algebra map `QuadraticAlgebra.lift`:

* `range_lift`: its range is the subalgebra generated by `u`;
* `lift_surjective_iff`: surjective iff `u` generates the algebra;
* `lift_injective_iff`: injective iff `1` and `u` are linearly independent.

Also add the basis decomposition `re_smul_add_im_smul` (used to golf `algHom_ext`) and `adjoin_omega_eq_top`.

Author: xroblot

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

@@ -5,8 +5,10 @@ Authors: Antoine Chambert-Loir
 -/
 module
 
+public import Mathlib.Algebra.Algebra.Subalgebra.Lattice
 public import Mathlib.Algebra.QuadraticAlgebra.Defs
 public import Mathlib.Algebra.Star.Unitary
+public import Mathlib.Tactic.FieldSimp.Lemmas
 
 import Mathlib.Tactic.FieldSimp
 
@@ -112,8 +114,9 @@ variable {A : Type*} [Ring A] [Algebra R A]
 @[ext]
 theorem algHom_ext {f g : QuadraticAlgebra R a b →ₐ[R] A}
     (h : f ω = g ω) : f = g := by
-  ext ⟨x, y⟩
-  simp [mk_eq_add_smul_omega, h]
+  refine AlgHom.ext fun z ↦ ?_
+  rw [← re_smul_add_im_smul z]
+  simp [h]
 
 /-- The unique `AlgHom` from `QuadraticAlgebra R a b` to an `R`-algebra `A`,
 constructed by replacing `ω` with the provided root.
@@ -164,8 +167,38 @@ def lift : { u : A // u * u = a • 1 + b • u } ≃ (QuadraticAlgebra R a b 
     ext
     simp
 
+/-- A quadratic algebra is generated by `ω`. -/
+theorem adjoin_omega_eq_top : Algebra.adjoin R {(ω : QuadraticAlgebra R a b)} = ⊤ :=
+  Algebra.eq_top_iff.mpr fun z ↦
+    re_smul_add_im_smul z ▸ add_mem (Subalgebra.smul_mem _ (one_mem _) _)
+      (Subalgebra.smul_mem _ (Algebra.self_mem_adjoin_singleton R ω) _)
+
+/-- The range of `lift ⟨u, h⟩` is the subalgebra of `A` generated by `u`. -/
+theorem range_lift {u : A} (h : u * u = a • 1 + b • u) :
+    (lift ⟨u, h⟩).range = Algebra.adjoin R {u} := by
+  rw [← Algebra.map_top, ← adjoin_omega_eq_top, AlgHom.map_adjoin_singleton]
+  simp
+
+/-- `lift ⟨u, h⟩` is surjective iff `u` generates `A` as an `R`-algebra. -/
+theorem lift_surjective_iff {u : A} (h : u * u = a • 1 + b • u) :
+    Function.Surjective (lift ⟨u, h⟩) ↔ Algebra.adjoin R {u} = ⊤ := by
+  rw [← AlgHom.range_eq_top, range_lift]
+
 end omega
 
+section lift
+
+variable [CommRing R] {A : Type*} [Ring A] [Algebra R A]
+
+/-- `lift ⟨u, h⟩` is injective iff `1` and `u` are `R`-linearly independent. -/
+theorem lift_injective_iff {u : A} (h : u * u = a • 1 + b • u) :
+    Function.Injective (lift ⟨u, h⟩) ↔ LinearIndependent R ![1, u] := by
+  rw [LinearIndependent.pair_iff, injective_iff_map_eq_zero]
+  refine ⟨fun hlift s t hst ↦ ?_, fun hlift z hz ↦ by ext <;> simp [hlift z.re z.im hz]⟩
+  simpa using QuadraticAlgebra.ext_iff.mp (hlift ⟨s, t⟩ (by rwa [lift_apply_apply]))
+
+end lift
+
 section star
 
 variable [CommRing R]