internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
apply prod_congr rfl
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
      (LinearForm.baseChange R S' M (b.coord x)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k x
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
      (LinearForm.baseChange R S' M (b.coord x)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k x
Tactic:
intro i _
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
rw [map_pow]
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) ^ k i =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) ^ k i =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
apply congr_arg₂ _ _ rfl
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m)
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
Proof 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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m)
Tactic:
rw [LinearForm.baseChange_compat_apply]
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof 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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : S ⊗[R] M
⊢ (polynomialMap b h).toFun S m = h.sum fun k n => (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] n
Tactic:
obtain ⟨n, ψ, p, rfl⟩ := PolynomialMap.exists_lift m
Proof state after:
case intro.intro.intro
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (polynomialMap b h).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (polynomialMap b h).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Tactic:
simp only [← isCompat_apply, toFun_eq_toFun', polynomialMap, polynomialMap_toFun, map_finsupp_sum]
Proof state after:
case intro.intro.intro
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (h.sum fun a b_1 =>
      (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ a i) ⊗ₜ[R] b_1)) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (h.sum fun a b_1 =>
      (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ a i) ⊗ₜ[R] b_1)) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Tactic:
apply Finsupp.sum_congr
Proof state after:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ x i) ⊗ₜ[R] h x) =
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ x i) ⊗ₜ[R] h x
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ x i) ⊗ₜ[R] h x) =
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ x i) ⊗ₜ[R] h x
Tactic:
intro k _
Proof state after:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N ψ.toLinearMap)
      ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k) =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N ψ.toLinearMap)
      ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k) =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Tactic:
rw [LinearMap.rTensor_tmul]
Proof state after:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Tactic:
congr
Proof state after:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
simp only [AlgHom.toLinearMap_apply, map_prod, map_pow]
Proof state after:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
apply prod_congr rfl
Proof state after:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
      (LinearForm.baseChange R S M (b.coord x)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k x
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
      (LinearForm.baseChange R S M (b.coord x)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k x
Tactic:
intro i _
Proof state after:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) ^ k i =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof state before:
case intro.intro.intro.h.e_m
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) ^ k i =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
apply congr_arg₂ _ _ rfl
Proof 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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p)
Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply
Proof 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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p)
Tactic:
rw [LinearForm.baseChange_compat_apply]
Proof state after:
no goals
Theorem: PolynomialMap.generize_finsupp_eq
Proof 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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
set m := Finset.sum univ (fun i => (X i : MvPolynomial ι R) ⊗ₜ[R] b i) with hm
Proof 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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Theorem: PolynomialMap.generize_finsupp_eq
Proof 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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [generize, coe_mk, AddHom.coe_mk, Finsupp.polynomialMap_toFun_apply]
Proof 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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (h.sum fun k n =>
      (∏ i : ι, (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (∑ i : ι, X i ⊗ₜ[R] b i) ^ k i) ⊗ₜ[R] n) =
    h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n