internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
have uFG : Subalgebra.FG (R := R) (φ R s).range := by
  rw [← Algebra.map_top]
  exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s.card)).out
Proof state after:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
set u' := rTensor M (φ R s').rangeRestrict.toLinearMap p' with hu'
Proof state after:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
have u'FG : Subalgebra.FG (R := R) (φ R s').range := by
  rw [← Algebra.map_top]
  exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s'.card)).out
Proof state after:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
have huu' : rTensor M (Subalgebra.val _).toLinearMap u =
  rTensor M (Subalgebra.val _).toLinearMap u' := by
  simp only [π] at h
  simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
    comp_rangeRestrict, h]
Proof state after:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
obtain ⟨B, hAB, hA'B, hB, h⟩ :=
  TensorProduct.Algebra.eq_of_fg_of_subtype_eq' (R := R) uFG u u'FG u' huu'
Proof state after:
case mk.mk.intro.intro.intro.intro
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (PolynomialMap.φ R s).range ≤ B
hA'B : (PolynomialMap.φ R s').range ≤ B
hB : B.FG
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk.intro.intro.intro.intro
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (PolynomialMap.φ R s).range ≤ B
hA'B : (PolynomialMap.φ R s').range ≤ B
hB : B.FG
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
obtain ⟨t, hB⟩ := hB
Proof state after:
case mk.mk.intro.intro.intro.intro.intro
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
huu' :
  (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (PolynomialMap.φ R s).range ≤ B
hA'B : (PolynomialMap.φ R s').range ≤ B
h :
  (LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap) u =
    (LinearMap.rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : Algebra.adjoin R ↑t = B
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
⊢ (PolynomialMap.φ R s).range.FG
Tactic:
rw [← Algebra.map_top]
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
⊢ (Subalgebra.map (PolynomialMap.φ R s) ⊤).FG
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
⊢ (Subalgebra.map (PolynomialMap.φ R s) ⊤).FG
Tactic:
exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s.card)).out
Proof state after:
no goals
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
⊢ (PolynomialMap.φ R s').range.FG
Tactic:
rw [← Algebra.map_top]
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
⊢ (Subalgebra.map (PolynomialMap.φ R s') ⊤).FG
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
⊢ (Subalgebra.map (PolynomialMap.φ R s') ⊤).FG
Tactic:
exact Subalgebra.FG.map _ (Algebra.FiniteType.mvPolynomial R (Fin s'.card)).out
Proof state after:
no goals
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
Tactic:
simp only [π] at h
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R s').toLinearMap) p'
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h :
  (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p =
    (LinearMap.rTensor M (PolynomialMap.φ R s').toLinearMap) p'
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
uFG : (PolynomialMap.φ R s).range.FG
u' : ↥(PolynomialMap.φ R s').range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (LinearMap.rTensor M (PolynomialMap.φ R s').rangeRestrict.toLinearMap) p'
u'FG : (PolynomialMap.φ R s').range.FG
⊢ (LinearMap.rTensor M (PolynomialMap.φ R s).range.val.toLinearMap) u =
    (LinearMap.rTensor M (PolynomialMap.φ R s').range.val.toLinearMap) u'
Tactic:
simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
  comp_rangeRestrict, h]
Proof state after:
no goals