Theorem: PolynomialMap.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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
have this := congr_fun (f.isCompat (MvPolynomial.aeval r))
  (univ.sum fun i => MvPolynomial.X i ⊗ₜ[R] m i)
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (⇑(LinearMap.rTensor N (aeval r).toLinearMap) ∘ f.toFun (MvPolynomial ι R)) (∑ i : ι, X i ⊗ₜ[R] m i) =
    (f.toFun S ∘ ⇑(LinearMap.rTensor M (aeval r).toLinearMap)) (∑ i : ι, X i ⊗ₜ[R] m i)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (⇑(LinearMap.rTensor N (aeval r).toLinearMap) ∘ f.toFun (MvPolynomial ι R)) (∑ i : ι, X i ⊗ₜ[R] m i) =
    (f.toFun S ∘ ⇑(LinearMap.rTensor M (aeval r).toLinearMap)) (∑ i : ι, X i ⊗ₜ[R] m i)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
simp only [Function.comp_apply, map_sum, LinearMap.rTensor_tmul,
  AlgHom.toLinearMap_apply, MvPolynomial.aeval_X] at this
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
let h := generize_eq m f
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n := generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n := generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk] at h
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
rw [← this, h, Finsupp.sum, _root_.map_sum]
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ ∑ x ∈ ((coeff m) f).support, (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
    ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ ∑ x ∈ ((coeff m) f).support, (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
    ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
apply sum_congr rfl
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ ∀ x ∈ ((coeff m) f).support,
    (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
      (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) x (((coeff m) f) x)

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
⊢ ∀ x ∈ ((coeff m) f).support,
    (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
      (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) x (((coeff m) f) x)
Tactic:
intro k _
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial k) 1 ⊗ₜ[R] ((coeff m) f) k) =
    (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) k (((coeff m) f) k)

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial k) 1 ⊗ₜ[R] ((coeff m) f) k) =
    (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) k (((coeff m) f) k)
Tactic:
simp only [LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply]
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) ⊗ₜ[R] ((coeff m) f) k = (∏ i : ι, r i ^ k i) ⊗ₜ[R] ((coeff m) f) k

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) ⊗ₜ[R] ((coeff m) f) k = (∏ i : ι, r i ^ k i) ⊗ₜ[R] ((coeff m) f) k
Tactic:
apply congr_arg₂ _ _ rfl
State after:
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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) = ∏ i : ι, r i ^ k i

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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) = ∏ i : ι, r i ^ k i
Tactic:
simp only [aeval_monomial, _root_.map_one, Finsupp.prod_pow, one_mul]
State after:
no goals