Theorem: PolynomialMap.isHomogeneousOfDegree_of_coeff_iff (DividedPowers/PolynomialMap/Homogeneous.lean)

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 : ℕ
⊢ IsHomogeneousOfDegree p f ↔ ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
Tactic:
refine ⟨fun hf _ m d hd => isHomogeneousOfDegree_coeff hf m d hd, fun H S _ _ r μ => ?_⟩
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
μ : S ⊗[R] M
⊢ f.toFun' S (r • μ) = r ^ p • f.toFun' S μ

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
μ : S ⊗[R] M
⊢ f.toFun' S (r • μ) = r ^ p • f.toFun' S μ
Tactic:
obtain ⟨n, s, m, rfl⟩ := TensorProduct.exists_Fin S μ
State after:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (r • ∑ i : Fin n, s i ⊗ₜ[R] m i) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)

State before:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (r • ∑ i : Fin n, s i ⊗ₜ[R] m i) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Tactic:
simp only [Finset.smul_sum, TensorProduct.smul_tmul']
State after:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (∑ x : Fin n, (r • s x) ⊗ₜ[R] m x) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)

State before:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ f.toFun' S (∑ x : Fin n, (r • s x) ⊗ₜ[R] m x) = r ^ p • f.toFun' S (∑ i : Fin n, s i ⊗ₜ[R] m i)
Tactic:
rw [← toFun_eq_toFun', image_eq_coeff_sum, image_eq_coeff_sum, Finsupp.smul_sum]
State after:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ (((coeff fun x => m x) f).sum fun k n_1 => (∏ i : Fin n, (r • s i) ^ k i) ⊗ₜ[R] n_1) =
    ((coeff fun i => m i) f).sum fun a b => r ^ p • (∏ i : Fin n, s i ^ a i) ⊗ₜ[R] b

State before:
case intro.intro.intro
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ (((coeff fun x => m x) f).sum fun k n_1 => (∏ i : Fin n, (r • s i) ^ k i) ⊗ₜ[R] n_1) =
    ((coeff fun i => m i) f).sum fun a b => r ^ p • (∏ i : Fin n, s i ^ a i) ⊗ₜ[R] b
Tactic:
apply Finsupp.sum_congr
State after:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ ∀ x ∈ ((coeff fun x => m x) f).support,
    (∏ i : Fin n, (r • s i) ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x =
      r ^ p • (∏ i : Fin n, s i ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x

State before:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
⊢ ∀ x ∈ ((coeff fun x => m x) f).support,
    (∏ i : Fin n, (r • s i) ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x =
      r ^ p • (∏ i : Fin n, s i ^ x i) ⊗ₜ[R] ((coeff fun x => m x) f) x
Tactic:
intro d hd
State after:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    r ^ p • (∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d

State before:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    r ^ p • (∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Tactic:
rw [TensorProduct.smul_tmul']
State after:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    (r ^ p • ∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d

State before:
case intro.intro.intro.h
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ i : Fin n, (r • s i) ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d =
    (r ^ p • ∏ i : Fin n, s i ^ d i) ⊗ₜ[R] ((coeff fun x => m x) f) d
Tactic:
apply congr_arg₂ _ _ rfl
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ i : Fin n, (r • s i) ^ d i = r ^ p • ∏ i : Fin n, s i ^ d i

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ i : Fin n, (r • s i) ^ d i = r ^ p • ∏ i : Fin n, s i ^ d i
Tactic:
simp only [smul_eq_mul, mul_pow, Finset.prod_mul_distrib]
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ x : Fin n, r ^ d x) * ∏ x : Fin n, s x ^ d x = r ^ p * ∏ i : Fin n, s i ^ d i

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ (∏ x : Fin n, r ^ d x) * ∏ x : Fin n, s x ^ d x = r ^ p * ∏ i : Fin n, s i ^ d i
Tactic:
apply congr_arg₂ _ _ rfl
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ x : Fin n, r ^ d x = r ^ p

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∏ x : Fin n, r ^ d x = r ^ p
Tactic:
rw [Finset.prod_pow_eq_pow_sum]
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ r ^ ∑ i : Fin n, d i = r ^ p

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ r ^ ∑ i : Fin n, d i = r ^ p
Tactic:
apply congr_arg₂ _ rfl
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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∑ i : Fin n, d i = p

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 : ℕ
H : ∀ (n : ℕ) (m : Fin n → M) (d : Fin n →₀ ℕ), (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
⊢ ∑ i : Fin n, d i = p
Tactic:
specialize H n m d
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 : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
⊢ ∑ i : Fin n, d i = p

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 : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : (d.sum fun x n => n) ≠ p → ((coeff m) f) d = 0
⊢ ∑ i : Fin n, d i = p
Tactic:
rw [not_imp_comm, Finsupp.sum_of_support_subset _ (Finset.subset_univ _) _ (fun _ _ ↦ rfl)] at H
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 : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : ¬((coeff m) f) d = 0 → ∑ x : Fin n, d x = p
⊢ ∑ i : Fin n, d i = p

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 : ℕ
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
n : ℕ
s : Fin n → S
m : Fin n → M
d : Fin n →₀ ℕ
hd : d ∈ ((coeff fun x => m x) f).support
H : ¬((coeff m) f) d = 0 → ∑ x : Fin n, d x = p
⊢ ∑ i : Fin n, d i = p
Tactic:
exact H (Finsupp.mem_support_iff.mp hd)
State after:
no goals