LeanPool.BrauerGroupNew.ExtendScalar

Imported Lean Pool material for LeanPool.BrauerGroupNew.ExtendScalar.

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)

Additive map sending l ⊗ a to l ⊗ (1 ⊗ a) after releasing scalars through K.

Equations

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

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)

Algebra homomorphism releasing an L ⊗[k] A tensor through K.

Equations

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

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 : L) : TensorProduct k K A →ₗ[k] TensorProduct k L A

Linear map sending m ⊗ a to (m • l) ⊗ a.

Equations

• absorbMap k K L A l = TensorProduct.lift { toFun := fun (m : K) => { toFun := fun (a : A) => (m • l) ⊗ₜ[k] a, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

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

Additive map absorbing the intermediate K tensor factor into L.

Equations

• absorbAddHom k K L A = TensorProduct.liftAddHom { toFun := fun (l : L) => ↑(absorbMap k K L A l), map_zero' := ⋯, map_add' := ⋯ } ⋯

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

Algebra homomorphism inverse to release, absorbing the intermediate K tensor factor.

Equations

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

def absorbEqv (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)

Algebra equivalence between direct scalar extension and extension through the intermediate field.

Equations

• absorbEqv 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 absorbEqv_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) : (absorbEqv k K L A) (l ⊗ₜ[k] a) = l ⊗ₜ[K] (1 ⊗ₜ[k] a)