English
If f is right inverse of g, then (linearEquivOfRightInverse hfg) x = f x.
Русский
Если f — правое обратное к g, то (linearEquivOfRightInverse hfg) x = f x.
LaTeX
$$linearEquivOfRightInverse hfg x = f x$$
Lean4
/-- If an `R`-algebra `A` is also an invertible `R`-module, then it is in fact isomorphic to the
base ring `R`. The algebra structure gives us a map `A ⊗ A → A`, which after tensoring by `Aᵛ`
becomes a map `A → R`, which is the inverse map we seek. -/
noncomputable def algEquivOfRing : R ≃ₐ[R] A :=
let inv : A →ₗ[R] R :=
linearEquiv R A ∘ₗ (LinearMap.mul' R A).lTensor (Dual R A) ∘ₗ (leftCancelEquiv A (linearEquiv R A)).symm
have right : inv ∘ₗ Algebra.linearMap R A = LinearMap.id :=
let ⟨s, hs⟩ := exists_finset ((linearEquiv R A).symm 1)
LinearMap.ext_ring <| by simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]
{ linearEquivOfRightInverse (f := Algebra.linearMap R A) (g := inv) (LinearMap.ext_iff.1 right),
Algebra.ofId R A with }
