English
The map lift provides a two-sided inverse between EvenHom Q A and (even Q →ₐ[R] A).
Русский
Карта lift задаёт биекцию между EvenHom Q A и (even Q →ₐ[R] A).
LaTeX
$$lift: EvenHom Q A ≃ (CliffordAlgebra.even Q →ₐ[R] A)$$
Lean4
/-- Two algebra morphisms from the even subalgebra are equal if they agree on pairs of generators.
See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext ⦃f g : even Q →ₐ[R] A⦄ (h : (even.ι Q).compr₂ f = (even.ι Q).compr₂ g) : f = g :=
by
rw [EvenHom.ext_iff] at h
ext ⟨x, hx⟩
induction x, hx using even_induction with
| algebraMap r => exact (f.commutes r).trans (g.commutes r).symm
| add x y hx hy ihx ihy =>
have := congr_arg₂ (· + ·) ihx ihy
exact (map_add f _ _).trans (this.trans <| (map_add g _ _).symm)
| ι_mul_ι_mul m₁ m₂ x hx
ih =>
have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)
