Theorem: MvPolynomial.rTensor_lcoeff (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
sn : MvPolynomial σ R ⊗[R] N
k : σ →₀ ℕ
⊢ (LinearMap.rTensor N (lcoeff R k)) sn = 1 ⊗ₜ[R] (scalarRTensor sn) k
Tactic:
induction sn using TensorProduct.induction_on with
| zero => simp
| tmul s n =>
  simp only [rTensor_tmul, scalarRTensor_apply_tmul, Finsupp.sum_apply]
  rw [Finsupp.sum_eq_single k (fun b _ hb => by rw [Finsupp.single_eq_of_ne hb])
    (fun _ => by rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
    Finsupp.single_eq_same, lcoeff_apply, ← smul_tmul, smul_eq_mul, mul_one]
  congr
| add x y hx hy => simp only [LinearMap.map_add, LinearEquiv.map_add, hx, hy,
    Finsupp.add_apply, tmul_add]
State after:
no goals

State before:
case zero
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
⊢ (LinearMap.rTensor N (lcoeff R k)) 0 = 1 ⊗ₜ[R] (scalarRTensor 0) k
Tactic:
simp
State after:
no goals

State before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (LinearMap.rTensor N (lcoeff R k)) (s ⊗ₜ[R] n) = 1 ⊗ₜ[R] (scalarRTensor (s ⊗ₜ[R] n)) k
Tactic:
simp only [rTensor_tmul, scalarRTensor_apply_tmul, Finsupp.sum_apply]
State after:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (lcoeff R k) s ⊗ₜ[R] n = 1 ⊗ₜ[R] Finsupp.sum s fun a₁ b => (Finsupp.single a₁ (b • n)) k

State before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ (lcoeff R k) s ⊗ₜ[R] n = 1 ⊗ₜ[R] Finsupp.sum s fun a₁ b => (Finsupp.single a₁ (b • n)) k
Tactic:
rw [Finsupp.sum_eq_single k (fun b _ hb => by rw [Finsupp.single_eq_of_ne hb])
  (fun _ => by rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
  Finsupp.single_eq_same, lcoeff_apply, ← smul_tmul, smul_eq_mul, mul_one]
State after:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ MvPolynomial.coeff k s ⊗ₜ[R] n = s k ⊗ₜ[R] n

State before:
case tmul
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
⊢ MvPolynomial.coeff k s ⊗ₜ[R] n = s k ⊗ₜ[R] n
Tactic:
congr
State after:
no goals

State before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
b : σ →₀ ℕ
x✝ : s b ≠ 0
hb : b ≠ k
⊢ (Finsupp.single b (s b • n)) k = 0
Tactic:
rw [Finsupp.single_eq_of_ne hb]
State after:
no goals

State before:
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
s : MvPolynomial σ R
n : N
x✝ : s k = 0
⊢ (Finsupp.single k (0 • n)) k = 0
Tactic:
rw [_root_.zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
State after:
no goals

State before:
case add
R : Type u
inst✝⁷ : CommRing R
M : Type uM
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type uN
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
ι : Type uι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
σ : Type u_1
inst✝ : DecidableEq σ
k : σ →₀ ℕ
x y : MvPolynomial σ R ⊗[R] N
hx : (LinearMap.rTensor N (lcoeff R k)) x = 1 ⊗ₜ[R] (scalarRTensor x) k
hy : (LinearMap.rTensor N (lcoeff R k)) y = 1 ⊗ₜ[R] (scalarRTensor y) k
⊢ (LinearMap.rTensor N (lcoeff R k)) (x + y) = 1 ⊗ₜ[R] (scalarRTensor (x + y)) k
Tactic:
simp only [LinearMap.map_add, LinearEquiv.map_add, hx, hy,
Finsupp.add_apply, tmul_add]
State after:
no goals