AlgEquiv API

Stream: Is there code for X?

[Kevin Buzzard]

Do we not have these? Do we want them? Have I got the names right?

import Mathlib

#check LinearEquiv.prodCongr -- (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M₄

def AlgEquiv.prodCongr {R A A₂ A₃ A₄ : Type*} [CommSemiring R]
    [Semiring A] [Semiring A₂] [Semiring A₃] [Semiring A₄] [Algebra R A]
    [Algebra R A₂] [Algebra R A₃] [Algebra R A₄]
    (e₁ : A ≃ₐ[R] A₂) (e₂ : A₃ ≃ₐ[R] A₄) :
    (A × A₃) ≃ₐ[R] (A₂ × A₄) where
  __ := LinearEquiv.prodCongr e₁.toLinearEquiv e₂.toLinearEquiv
  map_mul' := by simp
  commutes' := by simp

open scoped TensorProduct

#check TensorProduct.prodRight -- M₁ ⊗[R] (M₂ × M₃) ≃ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃

noncomputable def Algebra.TensorProduct.prodRight (R S A₁ A₂ A₃ : Type*)
    [CommSemiring R] [CommSemiring S] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R S]
    [Algebra R A₁] [Algebra S A₁] [IsScalarTower R S A₁] [Algebra R A₂] [Algebra R A₃] :
    A₁ ⊗[R] (A₂ × A₃) ≃ₐ[S] A₁ ⊗[R] A₂ × A₁ ⊗[R] A₃ where
  __ := _root_.TensorProduct.prodRight R S A₁ A₂ A₃
  map_mul' abc := by
    induction abc with
    | zero => simp
    | tmul x yz =>
      obtain ⟨y, z⟩ := yz
      intro abc
      induction abc with
      | zero => simp
      | tmul x y => simp
      | add x y _ _ => simp_all [add_mul, mul_add]
    | add x y _ _ => simp_all [add_mul, mul_add]
  commutes' s := by simp

[Aaron Liu]

docs#Algebra.TensorProduct.prodRight

[Kevin Buzzard]

Oh lol it was added 3 days ago and I didn't bump FLT for about 4 days :-) Thanks!

[Eric Wieser]

I think there is an open PR with this first result