internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof state before:
case h.e'_5.h.e'_6
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = ⇑f '' Set.range e
Tactic:
conv_rhs => rw [← Set.image_univ, Set.image_image, Set.image_univ]
Proof state after:
case h.e'_5.h.e'_6
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = Set.range fun x => f (e x)
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof state before:
case h.e'_5.h.e'_6
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ (Set.range fun s => 1 ⊗ₜ[R] e s) = Set.range fun x => f (e x)
Tactic:
rfl
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof state before:
case a.convert_2
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ Submodule.span R (Set.range e)
Tactic:
rw [hm]
Proof state after:
case a.convert_2
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ ⊤
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof state before:
case a.convert_2
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
r : S
m : M
h : r ⊗ₜ[R] m ∈ ⊤
f : M →ₗ[R] S ⊗[R] M := { toFun := fun m => 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
this : r ⊗ₜ[R] m = r • 1 ⊗ₜ[R] m
⊢ m ∈ ⊤
Tactic:
exact Submodule.mem_top
Proof state after:
no goals
Theorem: PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top
Proof state before:
case add
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 ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type u_1
e : σ → M
hm : Submodule.span R (Set.range e) = ⊤
x y : S ⊗[R] M
hx : x ∈ ⊤ → x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
hy : y ∈ ⊤ → y ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
h : x + y ∈ ⊤
⊢ x + y ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] e s)
Tactic:
exact Submodule.add_mem _ (hx Submodule.mem_top) (hy Submodule.mem_top)
Proof state after:
no goals
Theorem: PolynomialMap.coeff_injective
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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
⊢ f = g
Tactic:
ext S _ _ p
Proof state after:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ f.toFun' S p = g.toFun' S p
Theorem: PolynomialMap.coeff_injective
Proof state before:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ f.toFun' S p = g.toFun' S p
Tactic:
suffices hp : p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s) by
  simp only [Submodule.mem_span_iff_exists_sum _ p, TensorProduct.smul_tmul'] at hp
  obtain ⟨r, rfl⟩ := hp
  rw [Finsupp.sum_of_support_subset _ (subset_univ _) _ (fun  i _ => by
    rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul])]
  simp only [← toFun_eq_toFun'_apply, image_eq_coeff_sum, h]
Proof state after:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)
Theorem: PolynomialMap.coeff_injective
Proof state before:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)
Tactic:
rw [PolynomialMap.span_tensorProduct_eq_top_of_span_eq_top ι m hm]
Proof state after:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ ⊤
Theorem: PolynomialMap.coeff_injective
Proof state before:
case toFun'.h.h.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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
⊢ p ∈ ⊤
Tactic:
exact Submodule.mem_top
Proof state after:
no goals
Theorem: PolynomialMap.coeff_injective
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : p ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] m s)
⊢ f.toFun' S p = g.toFun' S p
Tactic:
simp only [Submodule.mem_span_iff_exists_sum _ p, TensorProduct.smul_tmul'] at hp
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : ∃ a, (a.sum fun i c => (c • 1) ⊗ₜ[R] m i) = p
⊢ f.toFun' S p = g.toFun' S p
Theorem: PolynomialMap.coeff_injective
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
p : S ⊗[R] M
hp : ∃ a, (a.sum fun i c => (c • 1) ⊗ₜ[R] m i) = p
⊢ f.toFun' S p = g.toFun' S p
Tactic:
obtain ⟨r, rfl⟩ := hp
Proof state after:
case intro
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i) = g.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i)
Theorem: PolynomialMap.coeff_injective
Proof state before:
case intro
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i) = g.toFun' S (r.sum fun i c => (c • 1) ⊗ₜ[R] m i)
Tactic:
rw [Finsupp.sum_of_support_subset _ (subset_univ _) _ (fun  i _ => by
  rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul])]
Proof state after:
case intro
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x) = g.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x)
Theorem: PolynomialMap.coeff_injective
Proof state before:
case intro
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x) = g.toFun' S (∑ x : ι, (r x • 1) ⊗ₜ[R] m x)
Tactic:
simp only [← toFun_eq_toFun'_apply, image_eq_coeff_sum, h]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_injective
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 ι
S✝ : Type v
inst✝² : CommRing S✝
inst✝¹ : Algebra R S✝
inst✝ : DecidableEq ι
m : ι → M
hm : Submodule.span R (Set.range m) = ⊤
f g : M →ₚ[R] N
h : (coeff m) f = (coeff m) g
S : Type u
x✝² : CommRing S
x✝¹ : Algebra R S
r : ι →₀ S
i : ι
x✝ : i ∈ univ
⊢ (0 • 1) ⊗ₜ[R] m i = 0
Tactic:
rw [smul_eq_mul, _root_.mul_one, TensorProduct.zero_tmul]
Proof state after:
no goals
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
⊢ ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S =
    polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)
Tactic:
ext m
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S) m =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S) m =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Tactic:
rw [Function.comp_apply, polynomialMap_toFun, Finsupp.sum, _root_.map_sum]
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∑ x ∈ h.support,
      (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∑ x ∈ h.support,
      (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Tactic:
apply sum_congr rfl
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
      (fun k n =>
          (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
        x (h x)
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
      (fun k n =>
          (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
        x (h x)
Tactic:
intro k _
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k) =
    (fun k n =>
        (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
      k (h k)
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k) =
    (fun k n =>
        (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
      k (h k)
Tactic:
simp only [LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply]
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] h k
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] h k
Tactic:
apply congr_arg₂ _ _ rfl
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
rw [map_prod φ]
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 ι
S✝ : Type v
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i