English
In a tower R → S → A with IsScalarTower, if an element r ∈ R is invertible in S then it is invertible in A; the corresponding inverse is compatible with the tower maps.
Русский
В башне башен R→S→A с условием IsScalarTower, если элемент r ∈ R обратим в S, то он обратим и в A; обратный образ совместим с картами башни.
LaTeX
$$$$ (algebraMap R A r) \text{ is invertible given invertible (algebraMap R S r) } $$$$
Lean4
/-- Suppose that `R → S → A` is a tower of algebras.
If an element `r : R` is invertible in `S`, then it is invertible in `A`. -/
def algebraTower (r : R) [Invertible (algebraMap R S r)] : Invertible (algebraMap R A r) :=
Invertible.copy (Invertible.map (algebraMap S A) (algebraMap R S r)) (algebraMap R A r)
(IsScalarTower.algebraMap_apply R S A r)
