internlm/Lean-Github huggingface dataset:
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case add.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
y : S ⊗[R] M
hy : ∃ m, y = m.sum fun s x => s ⊗ₜ[R] x
sx : S →₀ M
⊢ ∃ m, (sx.sum fun s x => s ⊗ₜ[R] x) + y = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
obtain ⟨sy, rfl⟩ := hy
Proof state after:
case add.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ∃ m, ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = m.sum fun s x => s ⊗ₜ[R] x
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case add.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ∃ m, ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = m.sum fun s x => s ⊗ₜ[R] x
Tactic:
use sx + sy
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = (sx + sy).sum fun s x => s ⊗ₜ[R] x
Theorem: TensorProduct.exists_Finsupp
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
⊢ ((sx.sum fun s x => s ⊗ₜ[R] x) + sy.sum fun s x => s ⊗ₜ[R] x) = (sx + sy).sum fun s x => s ⊗ₜ[R] x
Tactic:
rw [sum_add_index (fun _ ↦ by simp) (fun _ _ _ _ ↦ by rw [TensorProduct.tmul_add])]
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
x✝ : S
⊢ x✝ ∈ sx.support ∪ sy.support → x✝ ⊗ₜ[R] 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: TensorProduct.exists_Finsupp
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
sx sy : S →₀ M
x✝³ : S
x✝² : x✝³ ∈ sx.support ∪ sy.support
x✝¹ x✝ : M
⊢ x✝³ ⊗ₜ[R] (x✝¹ + x✝) = x✝³ ⊗ₜ[R] x✝¹ + x✝³ ⊗ₜ[R] x✝
Tactic:
rw [TensorProduct.tmul_add]
Proof state after:
no goals
Theorem: TensorProduct.exists_Fin
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
sm : S ⊗[R] M
⊢ ∃ n s m, sm = ∑ i : Fin n, s i ⊗ₜ[R] m i
Tactic:
obtain ⟨m, rfl⟩ := TensorProduct.exists_Finsupp S sm
Proof state after:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Theorem: TensorProduct.exists_Fin
Proof state before:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Tactic:
let e : m.support ≃ Fin (m.support.card) := Finset.equivFin _
Proof state after:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Theorem: TensorProduct.exists_Fin
Proof state before:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∃ n s m_1, (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin n, s i ⊗ₜ[R] m_1 i
Tactic:
use m.support.card, fun i ↦ e.symm i, fun i ↦ m (e.symm i)
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Theorem: TensorProduct.exists_Fin
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ (m.sum fun s x => s ⊗ₜ[R] x) = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Tactic:
rw [sum, ← Finset.sum_attach]
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∑ x ∈ m.support.attach, ↑x ⊗ₜ[R] m ↑x = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Theorem: TensorProduct.exists_Fin
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S →₀ M
e : { x // x ∈ m.support } ≃ Fin m.support.card := m.support.equivFin
⊢ ∑ x ∈ m.support.attach, ↑x ⊗ₜ[R] m ↑x = ∑ i : Fin m.support.card, ↑(e.symm i) ⊗ₜ[R] m ↑(e.symm i)
Tactic:
apply Finset.sum_equiv e <;> simp
Proof state after:
no goals
Theorem: TensorProduct.smul_rTensor
Proof state before:
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
m : S ⊗[R] M
⊢ φ s • (rTensor M φ.toLinearMap) m = (rTensor M φ.toLinearMap) (s • m)
Tactic:
induction m using TensorProduct.induction_on with
| zero => simp
| tmul s' m =>
  simp only [rTensor_tmul, AlgHom.toLinearMap_apply, smul_tmul', smul_eq_mul, _root_.map_mul]
| add m m' hm hm' => simp [hm, hm']
Proof state after:
no goals
Theorem: TensorProduct.smul_rTensor
Proof state before:
case zero
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s • (rTensor M φ.toLinearMap) 0 = (rTensor M φ.toLinearMap) (s • 0)
Tactic:
simp
Proof state after:
no goals
Theorem: TensorProduct.smul_rTensor
Proof state before:
case tmul
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s s' : S
m : M
⊢ φ s • (rTensor M φ.toLinearMap) (s' ⊗ₜ[R] m) = (rTensor M φ.toLinearMap) (s • s' ⊗ₜ[R] m)
Tactic:
simp only [rTensor_tmul, AlgHom.toLinearMap_apply, smul_tmul', smul_eq_mul, _root_.map_mul]
Proof state after:
no goals
Theorem: TensorProduct.smul_rTensor
Proof state before:
case add
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
m m' : S ⊗[R] M
hm : φ s • (rTensor M φ.toLinearMap) m = (rTensor M φ.toLinearMap) (s • m)
hm' : φ s • (rTensor M φ.toLinearMap) m' = (rTensor M φ.toLinearMap) (s • m')
⊢ φ s • (rTensor M φ.toLinearMap) (m + m') = (rTensor M φ.toLinearMap) (s • (m + m'))
Tactic:
simp [hm, hm']
Proof state after:
no goals
Theorem: TensorProduct.rTensor_smul'
Proof state before:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t
Tactic:
have : rTensor P (f.restrictScalars R) = (IsLinearMap.mk' _
  (TensorProduct.map_isLinearMap_of_left f LinearMap.id)).restrictScalars R := rfl
Proof state after:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
this : rTensor P (↑R f) = ↑R (IsLinearMap.mk' ⇑(map (↑R f) LinearMap.id) ⋯)
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t
Theorem: TensorProduct.rTensor_smul'
Proof state before:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
this : rTensor P (↑R f) = ↑R (IsLinearMap.mk' ⇑(map (↑R f) LinearMap.id) ⋯)
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t
Tactic:
rw [this, coe_restrictScalars, map_smul, IsLinearMap.mk'_apply]
Proof state after:
no goals
Theorem: PolynomialMap.IsHomogeneousOfDegree_add
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
f g : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
hg : IsHomogeneousOfDegree p g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ (f + g).toFun' S (s • m) = s ^ p • (f + g).toFun' S m
Tactic:
simp only [add_def_apply, smul_add, hf S s m, hg S s m]
Proof state after:
no goals
Theorem: PolynomialMap.IsHomogeneousOfDegree_smul
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ (r • f).toFun' S (s • m) = s ^ p • (r • f).toFun' S m
Tactic:
simp only [smul_def, Pi.smul_apply, hf S]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ r • s ^ p • f.toFun' S m = s ^ p • r • f.toFun' S m
Theorem: PolynomialMap.IsHomogeneousOfDegree_smul
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
r : R
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
s : S
m : S ⊗[R] M
⊢ r • s ^ p • f.toFun' S m = s ^ p • r • f.toFun' S m
Tactic:
exact smul_comm r (s ^ p) (toFun' f S m)
Proof state after:
no goals
Theorem: PolynomialMap.mem_grade
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₚ[R] N
p : ℕ
⊢ f ∈ grade p ↔ IsHomogeneousOfDegree p f
Tactic:
rfl
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_toFun
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m
Tactic:
choose n ψ  m' r' hm' hr' using PolynomialMap.exists_lift' m r
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m
Theorem: PolynomialMap.isHomogeneousOfDegree_toFun
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m
Tactic:
simp only [← hm', ← hr', ← isCompat_apply, toFun_eq_toFun', TensorProduct.smul_rTensor]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) (r' • m')) =
    ψ r' ^ p • (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) m')
Theorem: PolynomialMap.isHomogeneousOfDegree_toFun
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) (r' • m')) =
    ψ r' ^ p • (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) m')
Tactic:
rw [hf, ← TensorProduct.smul_rTensor, map_pow]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_ground
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
r : R
m : M
⊢ f.ground (r • m) = r ^ p • f.ground m
Tactic:
simp only [ground, Function.comp_apply, map_smul, TensorProduct.lid_symm_apply, hf R r]
Proof state after:
no goals
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
⊢ ((coeff m) f) d = 0
Tactic:
let e (b : ι →₀ ℕ) (k : ℕ) : Option ι →₀ ℕ :=
  Finsupp.update (Finsupp.mapDomainEmbedding (Function.Embedding.some) b) none k
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
⊢ ((coeff m) f) d = 0
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
⊢ ((coeff m) f) d = 0
Tactic:
have he : ∀ b k, (X none ^ k * (Finset.prod Finset.univ
  fun x => X (some x) ^ b x) : MvPolynomial (Option ι) R) = monomial (e b k) 1 := fun b k ↦ by
  rw [monomial_eq, Finsupp.prod_pow, Fintype.prod_option, _root_.map_one, one_mul]
  simp only [Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply, Finsupp.coe_update,
    Function.update_same, ne_eq, not_false_eq_true, Function.update_noteq, e]
  exact congr_arg₂ _ rfl (Finset.prod_congr rfl (fun _ _ => by
    rw [Finsupp.mapDomain_apply (Option.some_injective ι)]))
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
⊢ ((coeff m) f) d = 0
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
⊢ ((coeff m) f) d = 0
Tactic:
have he_some : ∀ b k i, e b k (some i) = b i := fun b k i ↦ by
  simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
    Finsupp.coe_mk, Function.update, ↓reduceDite,
    Finsupp.mapDomain_apply (Option.some_injective ι), e]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
⊢ ((coeff m) f) d = 0
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
⊢ ((coeff m) f) d = 0
Tactic:
have he_none : ∀ b k, k = e b k none := fun b k ↦ by
  simp only [Finsupp.update, Finsupp.mapDomainEmbedding_apply, Function.Embedding.some_apply,
    Finsupp.coe_mk, Function.update, ↓reduceDite, e]
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
⊢ ((coeff m) f) d = 0
Theorem: PolynomialMap.isHomogeneousOfDegree_coeff
Proof state before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
⊢ ((coeff m) f) d = 0
Tactic:
let μ : MvPolynomial (Option ι) R ⊗[R] M := Finset.univ.sum (fun i => X (some i) ⊗ₜ[R] m i)
Proof state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
hf : IsHomogeneousOfDegree p f
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
d : ι →₀ ℕ
hd : (d.sum fun x n => n) ≠ p
e : (ι →₀ ℕ) → ℕ → Option ι →₀ ℕ := fun b k => ((Finsupp.mapDomainEmbedding Function.Embedding.some) b).update none k
he : ∀ (b : ι →₀ ℕ) (k : ℕ), X none ^ k * ∏ x : ι, X (some x) ^ b x = (monomial (e b k)) 1
he_some : ∀ (b : ι →₀ ℕ) (k : ℕ) (i : ι), (e b k) (some i) = b i
he_none : ∀ (b : ι →₀ ℕ) (k : ℕ), k = (e b k) none
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
⊢ ((coeff m) f) d = 0