-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
/--
Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ A`, the centralizer of `S ⊗ 1 ⊆ A ⊗ B` is `C_A(S) ⊗ B` where `C_A(S)` is the
centralizer of `S` in `A`.
-/
lemma centralizer_coe_image_includeLeft_eq_center_tensorProduct
    (S : Set A) [Module.Free R B] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.includeLeft (S := R) '' S) =
    (Algebra.TensorProduct.map (Subalgebra.centralizer R (S : Set A)).val
      (AlgHom.id R B)).range

Proof state:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m => m ⊗ₜ[R] ℬ i) = (b.sum fun i m => m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ x • b = mapRange (fun x_1 => x_1 * x) ⋯ b

Tactic:
specialize hw (x ⊗ₜ[R] 1) ⟨x, hx, rfl⟩

Result:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : (x ⊗ₜ[R] 1 * b.sum fun i m => m ⊗ₜ[R] ℬ i) = (b.sum fun i m => m ⊗ₜ[R] ℬ i) * x ⊗ₜ[R] 1
⊢ x • b = mapRange (fun x_1 => x_1 * x) ⋯ b

Proof state:
case h.mpr.intro.intro.intro.add
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
y z : ↥(centralizer R S) ⊗[R] B
hy :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom y * includeLeft x
hz :
  includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom z * includeLeft x
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (y + z) * includeLeft x

Tactic:
rw [map_add, mul_add, hy, hz, add_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ ∀ i ∈ b.support, ((TensorProduct.mk R A B).flip (ℬ i)) 0 = 0

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
⊢ centralizer R (⇑includeLeft '' S) = (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Tactic:
ext w

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ centralizer R (⇑includeLeft '' S) ↔ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ centralizer R (⇑includeLeft '' S) ↔ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ centralizer R (⇑includeLeft '' S) → w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

case h.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range → w ∈ centralizer R (⇑includeLeft '' S)

Proof state:
case h.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ centralizer R (⇑includeLeft '' S) → w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Tactic:
intro hw

Result:
case h.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
hw : w ∈ centralizer R (⇑includeLeft '' S)
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Proof state:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m => m ⊗ₜ[R] ℬ i) = (b.sum fun i m => m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
⊢ ∀ g ∈ S, g * b j = b j * g

Tactic:
intro x hx

Result:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m => m ⊗ₜ[R] ℬ i) = (b.sum fun i m => m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ x * b j = b j * x

Proof state:
case h.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : A ⊗[R] B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range → w ∈ centralizer R (⇑includeLeft '' S)

Tactic:
rintro ⟨w, rfl⟩

Result:
case h.mpr.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w ∈ centralizer R (⇑includeLeft '' S)