internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h.a
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
      lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)) =
    lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap)
Tactic:
apply TensorProduct.lift.unique
Proof state after:
case h.a.H
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ∀ (x : S[X]) (y : N),
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
          lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
        (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) x) y
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h.a.H
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
⊢ ∀ (x : S[X]) (y : N),
    (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
          lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
        (x ⊗ₜ[R] y) =
      (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) x) y
Tactic:
intro f n
Proof state after:
case h.a.H
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
        lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
      (f ⊗ₜ[R] n) =
    (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) f) n
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h.a.H
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (↑R (IsLinearMap.mk' (fun z => s ^ p • z) ⋯) ∘ₗ
        lift ((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p)))
      (f ⊗ₜ[R] n) =
    (((TensorProduct.mk R S N).compl₂ LinearMap.id ∘ₗ ↑R (lcoeff S p) ∘ₗ ψ.toLinearMap) f) n
Tactic:
simp only [compl₂_id, coe_comp, coe_restrictScalars, Function.comp_apply, lift.tmul,
  lcoeff_apply, mk_apply, IsLinearMap.mk'_apply, AlgHom.toLinearMap_apply,
  AlgHom.coe_restrictScalars', TensorProduct.smul_tmul']
Proof state after:
case h.a.H
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (s ^ p • f.coeff p) ⊗ₜ[R] n = (ψ f).coeff p ⊗ₜ[R] n
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h.a.H
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ (s ^ p • f.coeff p) ⊗ₜ[R] n = (ψ f).coeff p ⊗ₜ[R] n
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ s ^ p • f.coeff p = (ψ f).coeff p
Theorem: PolynomialMap.componentIsHomogeneous
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
f : S[X]
n : N
⊢ s ^ p • f.coeff p = (ψ f).coeff p
Tactic:
induction f using Polynomial.induction_on' with
| h_add f g hf hg => rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
| h_monomial n a =>
    simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
      one_mul, coeff_monomial]
    split_ifs with h
    . rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
        one_mul, ← C_eq_algebraMap]
      simp only [C_mul_monomial, coeff_monomial, if_pos]
    . simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
        monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h_add
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
f✝¹ : M →ₚ[R] N
p✝ p : ℕ
f✝ : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n : N
f g : S[X]
hf : s ^ p • f.coeff p = (ψ f).coeff p
hg : s ^ p • g.coeff p = (ψ g).coeff p
⊢ s ^ p • (f + g).coeff p = (ψ (f + g)).coeff p
Tactic:
rw [coeff_add, smul_add, hf, hg, ← coeff_add, map_add]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h_monomial
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ s ^ p • ((monomial n) a).coeff p = (ψ ((monomial n) a)).coeff p
Tactic:
simp only [ψ, aeval_monomial, ← smul_eq_mul, algebraMap_smul, coeff_smul, monomial_pow,
  one_mul, coeff_monomial]
Proof state after:
case h_monomial
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ (s ^ p • if n = p then a else 0) = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h_monomial
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
⊢ (s ^ p • if n = p then a else 0) = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
split_ifs with h
Proof state after:
case pos
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

case neg
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case pos
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p

case neg
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
. rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
    one_mul, ← C_eq_algebraMap]
  simp only [C_mul_monomial, coeff_monomial, if_pos]
Proof state after:
case neg
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case neg
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
. simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
    monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case pos
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ s ^ p • a = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
rw [smul_eq_mul, mul_comm, h, AlgHom.coe_restrictScalars', aeval_monomial, monomial_pow,
  one_mul, ← C_eq_algebraMap]
Proof state after:
case pos
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ a * s ^ p = (C a * (monomial p) (s ^ p)).coeff p
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case pos
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : n = p
⊢ a * s ^ p = (C a * (monomial p) (s ^ p)).coeff p
Tactic:
simp only [C_mul_monomial, coeff_monomial, if_pos]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case neg
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
this :
  (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
t : S[X] ⊗[R] N
n✝ : N
n : ℕ
a : S
h : ¬n = p
⊢ s ^ p • 0 = ((AlgHom.restrictScalars R (aeval ((monomial 1) s))) ((monomial n) a)).coeff p
Tactic:
simp only [smul_zero, AlgHom.coe_restrictScalars', aeval_monomial, ← C_eq_algebraMap,
  monomial_pow, one_mul, C_mul_monomial, coeff_monomial, if_neg h]
Proof state after:
no goals
Theorem: PolynomialMap.componentIsHomogeneous
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ (LinearMap.rTensor M (↑R (monomial 1))) (s • sm) =
    (LinearMap.rTensor M ψ.toLinearMap) ((LinearMap.rTensor M (↑R (monomial 1))) sm)
Tactic:
suffices ∀ (sm : S ⊗[R] M), s • sm =
    rTensor M (((IsLinearMap.isLinearMap_smul s).mk').restrictScalars R) sm by
  simp only [this, ← rTensor_comp_apply]
  apply LinearMap.congr_fun
  apply congr_arg
  rw [LinearMap.ext_iff]
  intro r
  simp only [compl₂_id, smul_eq_mul, lift.tmul, coe_comp, coe_restrictScalars,
    Function.comp_apply, IsLinearMap.mk'_apply, mk_apply, AlgHom.toLinearMap_apply,
    AlgHom.coe_restrictScalars', aeval_monomial, pow_one]
  rw [mul_comm]
  simp only [AlgHom.coe_restrictScalars', aeval_monomial, pow_one, ψ, ← smul_eq_mul,
    algebraMap_smul, Polynomial.smul_monomial]
Proof state after:
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Theorem: PolynomialMap.componentIsHomogeneous
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
⊢ ∀ (sm : S ⊗[R] M), s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
intro sm
Proof state after:
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Theorem: PolynomialMap.componentIsHomogeneous
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ s • sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
rw [← (IsLinearMap.isLinearMap_smul s).mk'_apply, ← LinearMap.coe_restrictScalars R]
Proof state after:
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Theorem: PolynomialMap.componentIsHomogeneous
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ (↑R (IsLinearMap.mk' (fun z => s • z) ⋯)) sm = (LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))) sm
Tactic:
apply LinearMap.congr_fun
Proof state after:
case h
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))
Theorem: PolynomialMap.componentIsHomogeneous
Proof state before:
case h
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) = LinearMap.rTensor M (↑R (IsLinearMap.mk' (fun z => s • z) ⋯))
Tactic:
dsimp only [LinearMap.rTensor, TensorProduct.map, smul_eq_mul]
Proof state after:
case h
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
f✝ : M →ₚ[R] N
p✝ p : ℕ
f : M →ₚ[R] N
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
sm✝ : S ⊗[R] M
ψ : S[X] →ₐ[R] S[X] := AlgHom.restrictScalars R (aeval ((monomial 1) s))
sm : S ⊗[R] M
⊢ ↑R (IsLinearMap.mk' (fun z => s • z) ⋯) =
    lift ((TensorProduct.mk R S M).compl₂ LinearMap.id ∘ₗ ↑R (IsLinearMap.mk' (fun z => s * z) ⋯))