The algebra generated by an element and its inverse

If F * G = 1 in a commutative R-algebra, every monomial Fⁱ Gʲ is Fⁱ⁻ʲ or Gʲ⁻ⁱ. Hence the subalgebra R[F, G] is, as an R-submodule, the sum of R[F] and R[G]: every element of R[F, G] is a polynomial in F plus a polynomial in G. This is the decomposition of a Laurent polynomial into its parts of nonnegative and of negative degree, for the image of R[T, T⁻¹] under T ↦ F.

Main results

• TauCeti.Algebra.toSubmodule_adjoin_pair_eq_sup_of_mul_eq_one: if F * G = 1, then R[F, G] = R[F] + R[G] as R-submodules.

theorem TauCeti.Algebra.toSubmodule_adjoin_pair_eq_sup_of_mul_eq_one {R : Type u_1} {B : Type u_2} [CommSemiring R] [CommSemiring B] [Algebra R B] {F G : B} (hFG : F * G = 1) : Subalgebra.toSubmodule R[F, G] = Subalgebra.toSubmodule R[F] ⊔ Subalgebra.toSubmodule R[G]

An algebra generated by an element and an inverse. If F * G = 1, the subalgebra R[F, G] is, as an R-submodule, the sum of R[F] and R[G]: every element of R[F, G] is an element of R[F] plus an element of R[G]. Compare Algebra.adjoin_union_coe_submodule, which for arbitrary F and G describes the same submodule as the product R[F] * R[G].