English
The isomorphism is established by a standard tensor product construction on subalgebras.
Русский
Изоморфизм доказывается обычной конструкцией тензорного произведения над подалгебрами.
LaTeX
$$$A.lTensorBot \\cong_R A$$$
Lean4
/-- If `A` is a subalgebra of `S/R`, there is the natural `R`-algebra isomorphism between
`A ⊗[R] i(R)` and `A` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `Algebra.TensorProduct.rid` as `i(R)` is not necessarily isomorphic to `R`.
This is the `Subalgebra` version of `Submodule.rTensorOne` -/
def rTensorBot : A ⊗[R] (⊥ : Subalgebra R S) ≃ₐ[R] A :=
by
refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).rTensorOne ?_ ?_
· rintro a b x y
obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2
replace hx : algebraMap R _ x' = x := Subtype.val_injective hx
obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2
replace hy : algebraMap R _ y' = y := Subtype.val_injective hy
rw [← hx, ← hy, ← map_mul]
erw [(toSubmodule A).rTensorOne_tmul x' a, (toSubmodule A).rTensorOne_tmul y' b,
(toSubmodule A).rTensorOne_tmul (x' * y') (a * b)]
rw [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']
· exact Submodule.rTensorOne_tmul_one _
