English
If A is a subalgebra of S over R, there is a natural R-algebra isomorphism between ⊥ ⊗_R A and A given by multiplication in S.
Русский
Для подалгебры A ⊆ S/R существует естественный изоморфизм по R: ⊥ ⊗_R A ≅ A, индуцируемый умножением в S.
LaTeX
$$$(\\perp_R) ⊗_R A \\cong_R A$$$
Lean4
/-- If `A` is a subalgebra of `S/R`, there is the natural `R`-algebra isomorphism between
`i(R) ⊗[R] A` and `A` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `Algebra.TensorProduct.lid` as `i(R)` is not necessarily isomorphic to `R`.
This is the `Subalgebra` version of `Submodule.lTensorOne` -/
def lTensorBot : (⊥ : Subalgebra R S) ⊗[R] A ≃ₐ[R] A :=
by
refine Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (toSubmodule A).lTensorOne ?_ ?_
· rintro x y a b
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).lTensorOne_tmul x' a, (toSubmodule A).lTensorOne_tmul y' b,
(toSubmodule A).lTensorOne_tmul (x' * y') (a * b)]
rw [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']
· exact Submodule.lTensorOne_one_tmul _
