internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.lfsum_eq
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_3
f : ι → M →ₚ[R] N
hf : LocFinsupp f
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (lfsum f).toFun' S m = (Finsupp.ofSupportFinite (fun i => (f i).toFun' S m) ⋯).sum fun x m => m
Tactic:
rw [lfsum, dif_pos hf]
Proof state after:
no goals
Theorem: PolynomialMap.generize_comp_equiv
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Tactic:
let hf := f.isCompat_apply (aeval (fun i ↦ X (e i)) : MvPolynomial ι R →ₐ[R] MvPolynomial κ R)
  (univ.sum (fun i ↦ X i ⊗ₜ[R] (m (e 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Theorem: PolynomialMap.generize_comp_equiv
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Tactic:
simp only [map_sum, rTensor_tmul, AlgHom.toLinearMap_apply, aeval_X] at hf
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Theorem: PolynomialMap.generize_comp_equiv
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk, comp_apply, hf]
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i) = f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
Theorem: PolynomialMap.generize_comp_equiv
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i) = f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
Tactic:
apply congr_arg
Proof state after:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : ι, X (e x) ⊗ₜ[R] m (e x)
Theorem: PolynomialMap.generize_comp_equiv
Proof state before:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : ι, X (e x) ⊗ₜ[R] m (e x)
Tactic:
simp only [sum_congr_equiv e, map_univ_equiv]
Proof state after:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : κ, ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x
Theorem: PolynomialMap.generize_comp_equiv
Proof state before:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : κ, ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x
Tactic:
exact sum_congr rfl (fun k _ => by rw [Function.comp_apply, Equiv.apply_symm_apply])
Proof state after:
no goals
Theorem: PolynomialMap.generize_comp_equiv
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
k : κ
x✝ : k ∈ univ
⊢ X k ⊗ₜ[R] m k = ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) k
Tactic:
rw [Function.comp_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: PolynomialMap.generize_comp_equiv'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
let hf' := f.isCompat_apply
  (aeval (fun i ↦ X (e.symm i)) : MvPolynomial κ R →ₐ[R] MvPolynomial ι R)
  (univ.sum (fun i ↦ X i ⊗ₜ[R] (m 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' : (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
    (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
  f.toFun (MvPolynomial ι R)
    ((LinearMap.rTensor M (aeval fun i => X (e.symm i)).toLinearMap) (∑ i : κ, X i ⊗ₜ[R] m i)) :=
  isCompat_apply f (aeval fun i => X (e.symm i)) (∑ i : κ, X i ⊗ₜ[R] m i)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Theorem: PolynomialMap.generize_comp_equiv'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' : (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
    (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
  f.toFun (MvPolynomial ι R)
    ((LinearMap.rTensor M (aeval fun i => X (e.symm i)).toLinearMap) (∑ i : κ, X i ⊗ₜ[R] m i)) :=
  isCompat_apply f (aeval fun i => X (e.symm i)) (∑ i : κ, X i ⊗ₜ[R] m i)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
simp only [map_sum, rTensor_tmul, AlgHom.toLinearMap_apply, aeval_X] at hf'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Theorem: PolynomialMap.generize_comp_equiv'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk, hf']
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
Theorem: PolynomialMap.generize_comp_equiv'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
Tactic:
apply congr_arg
Proof state after:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : ι, X x ⊗ₜ[R] m (e x) = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Theorem: PolynomialMap.generize_comp_equiv'
Proof state before:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : ι, X x ⊗ₜ[R] m (e x) = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Tactic:
simp only [sum_congr_equiv e, map_univ_equiv]
Proof state after:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : κ, ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Theorem: PolynomialMap.generize_comp_equiv'
Proof state before:
case 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : κ, ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Tactic:
exact sum_congr rfl (fun k _ => by rw [Function.comp_apply, Equiv.apply_symm_apply])
Proof state after:
no goals
Theorem: PolynomialMap.generize_comp_equiv'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
k : κ
x✝ : k ∈ univ
⊢ ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) k = X (e.symm k) ⊗ₜ[R] m k
Tactic:
rw [Function.comp_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: PolynomialMap.generize_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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
dsimp only [coeff, coe_comp, LinearEquiv.coe_coe, Function.comp_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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = (scalarRTensor ((generize m) f)).sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Theorem: PolynomialMap.generize_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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = (scalarRTensor ((generize m) f)).sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
generalize h : scalarRTensor (generize m f) = p
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor ((generize m) f) = p
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Theorem: PolynomialMap.generize_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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor ((generize m) f) = p
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [eq_comm, ← LinearEquiv.symm_apply_eq] at h
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Theorem: PolynomialMap.generize_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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [← h, LinearEquiv.symm_apply_eq, map_finsupp_sum]
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ p = p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)
Theorem: PolynomialMap.generize_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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ p = p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)
Tactic:
ext d
Proof state after:
case 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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = (p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)) d
Theorem: PolynomialMap.generize_eq
Proof state before:
case 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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = (p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)) d
Tactic:
rw [Finsupp.sum_apply, Finsupp.sum_eq_single d, scalarRTensor_apply_tmul_apply,
  coeff_monomial, if_pos rfl, _root_.one_smul]
Proof state after:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ ∀ (b : ι →₀ ℕ), p b ≠ 0 → b ≠ d → (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0

case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = 0 → (scalarRTensor ((monomial d) 1 ⊗ₜ[R] 0)) d = 0
Theorem: PolynomialMap.generize_eq
Proof state before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ ∀ (b : ι →₀ ℕ), p b ≠ 0 → b ≠ d → (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0
Tactic:
intro b _ hb
Proof state after:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d b : ι →₀ ℕ
a✝ : p b ≠ 0
hb : b ≠ d
⊢ (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0
Theorem: PolynomialMap.generize_eq
Proof state before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d b : ι →₀ ℕ
a✝ : p b ≠ 0
hb : b ≠ d
⊢ (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0
Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_monomial, if_neg hb, _root_.zero_smul]
Proof state after:
no goals
Theorem: PolynomialMap.generize_eq
Proof state before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = 0 → (scalarRTensor ((monomial d) 1 ⊗ₜ[R] 0)) d = 0
Tactic:
simp only [tmul_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, implies_true]
Proof state after:
no goals