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
μ : MvPolynomial (Option ι) R ⊗[R] M := ∑ i : ι, X (some i) ⊗ₜ[R] m i
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = 0
⊢ ((coeff m) f) d = 0

case hnc
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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)

case hc
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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)

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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0
Tactic:
exact hφ
Proof state after:
case hnc
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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ : ((coeff fun i => m i) f) d = (if e d p = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d
⊢ ¬e d p = e d (d.sum fun x n => n)

case hc
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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (if e d (∑ i : ι, d i) = e d (d.sum fun x n => n) then 1 else 0) • ((coeff fun i => m i) f) d =
    MvPolynomial.coeff (e d (d.sum fun x n => n)) (X none ^ p * ∏ i : ι, X (some i) ^ d i) • ((coeff fun i => m i) f) d
⊢ e d (∑ i : ι, d i) = e d (d.sum fun x n => n)

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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  φ (((X none ^ ∑ i : ι, d i) * ∏ x : ι, X (some x) ^ d x) ⊗ₜ[R] ((coeff fun i => m i) f) d) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ ((X none ^ p * ∏ i : ι, X (some i) ^ b i) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0

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
hf' :
  (((coeff fun i => m i) f).sum fun k n => (∏ i : ι, (X none • X (some i)) ^ k i) ⊗ₜ[R] n) =
    ((coeff fun i => m i) f).sum fun a b => (X none ^ p • ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b
φ : MvPolynomial (Option ι) R ⊗[R] N →ₗ[R] N :=
  ↑(TensorProduct.lid R N) ∘ₗ LinearMap.rTensor N (lcoeff R (e d (d.sum fun x n => n)))
hφ :
  (((coeff fun i => m i) f).sum fun a b => φ (((X none ^ ∑ i : ι, a i) * ∏ x : ι, X (some x) ^ a x) ⊗ₜ[R] b)) =
    ((coeff fun i => m i) f).sum fun a b => φ ((X none ^ p * ∏ i : ι, X (some i) ^ a i) ⊗ₜ[R] b)
⊢ ∀ (b : ι →₀ ℕ),
    ((coeff fun i => m i) f) b ≠ 0 →
      b ≠ d → φ (((X none ^ ∑ i : ι, b i) * ∏ x : ι, X (some x) ^ b x) ⊗ₜ[R] ((coeff fun i => m i) f) b) = 0