Theorem: PolynomialMap.ground_image_eq_coeff_sum (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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ f.ground (∑ i : ι, r i • m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n
Tactic:
apply (TensorProduct.lid R N).symm.injective
State after:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (TensorProduct.lid R N).symm (f.ground (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)

State before:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (TensorProduct.lid R N).symm (f.ground (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Tactic:
rw [TensorProduct.lid_symm_apply, isCompat_apply_ground, ← TensorProduct.lid_symm_apply]
State after:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ f.toFun R ((TensorProduct.lid R M).symm (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)

State before:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ f.toFun R ((TensorProduct.lid R M).symm (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Tactic:
simp only [map_sum, TensorProduct.lid_symm_apply, ← TensorProduct.smul_tmul, smul_eq_mul, mul_one]
State after:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ f.toFun R (∑ x : ι, r x ⊗ₜ[R] m x) = 1 ⊗ₜ[R] ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n

State before:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ f.toFun R (∑ x : ι, r x ⊗ₜ[R] m x) = 1 ⊗ₜ[R] ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n
Tactic:
rw [image_eq_coeff_sum, ← TensorProduct.lid_symm_apply, map_finsupp_sum]
State after:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => (TensorProduct.lid R N).symm ((∏ i : ι, r i ^ a i) • b)

State before:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => (TensorProduct.lid R N).symm ((∏ i : ι, r i ^ a i) • b)
Tactic:
simp only [map_finsupp_sum, TensorProduct.lid_symm_apply]
State after:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => 1 ⊗ₜ[R] ((∏ i : ι, r i ^ a i) • b)

State before:
case a
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => 1 ⊗ₜ[R] ((∏ i : ι, r i ^ a i) • b)
Tactic:
exact Finsupp.sum_congr (fun d _ => by rw [← TensorProduct.smul_tmul, smul_eq_mul, mul_one])
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 ι
m : ι → M
f : M →ₚ[R] N
r : ι → R
d : ι →₀ ℕ
x✝ : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : ι, r i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d = 1 ⊗ₜ[R] ((∏ i : ι, r i ^ d i) • ((coeff fun x => m x) f) d)
Tactic:
rw [← TensorProduct.smul_tmul, smul_eq_mul, mul_one]
State after:
no goals