noncomputable def releaseAddHom (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : TensorProduct k L A →+ TensorProduct K L (TensorProduct k K A)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def release (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : TensorProduct k L A →ₐ[L] TensorProduct K L (TensorProduct k K A)

Equations

• release k K L A = { toFun := (↑(releaseAddHom k K L A)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def absorbMap (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : L → TensorProduct k K A →+ TensorProduct k L A

Equations

• One or more equations did not get rendered due to their size.

noncomputable def absorbAddHom (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : TensorProduct K L (TensorProduct k K A) →+ TensorProduct k L A

Equations

• absorbAddHom k K L A = TensorProduct.liftAddHom { toFun := absorbMap k K L A, map_zero' := ⋯, map_add' := ⋯ } ⋯

noncomputable def absorb (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : TensorProduct K L (TensorProduct k K A) →ₐ[L] TensorProduct k L A

Equations

• absorb k K L A = { toFun := (↑(absorbAddHom k K L A)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def absorb_eqv (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] : TensorProduct k L A ≃ₐ[L] TensorProduct K L (TensorProduct k K A)

Equations

• absorb_eqv k K L A = { toFun := ⇑(release k K L A), invFun := ⇑(absorb k K L A), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem absorb_eqv_apply (k K L A : Type u) [Field k] [Field K] [Field L] [Algebra k K] [Algebra K L] [Algebra k L] [Ring A] [Algebra k A] [IsScalarTower k K L] (l : L) (a : A) : (absorb_eqv k K L A) (l ⊗ₜ[k] a) = l ⊗ₜ[K] 1 ⊗ₜ[k] a