internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk.intro.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 : B = (PolynomialMap.φ R t).range
hAB' : (PolynomialMap.φ R s).range ≤ (PolynomialMap.φ R t).range
hA'B' : (PolynomialMap.φ R s').range ≤ (PolynomialMap.φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (LinearMap.rTensor M (Subalgebra.inclusion hA'B').toLinearMap) u' =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hA'B)).toLinearMap) u'
Tactic:
congr
Proof state after:
no goals
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk.intro.intro.intro.intro.intro.intro.e_a.e_f.a.h.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✝ 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 : B = (PolynomialMap.φ R t).range
hAB' : (PolynomialMap.φ R s).range ≤ (PolynomialMap.φ R t).range
hA'B' : (PolynomialMap.φ R s').range ≤ (PolynomialMap.φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (LinearMap.rTensor M (PolynomialMap.φ R t).rangeRestrict.toLinearMap) q =
    (LinearMap.rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
x✝¹ : ↥(PolynomialMap.φ R s).range
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry (LinearMap.rTensor M (Subalgebra.inclusion hAB').toLinearMap)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          (LinearMap.rTensor M (Subalgebra.inclusion ⋯).toLinearMap ∘ₗ
            LinearMap.rTensor M (Subalgebra.inclusion hAB).toLinearMap))
        x✝¹)
      x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: PolynomialMap.toFun_eq_toFunLifted_apply
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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun S t = (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)
Tactic:
rw [PolynomialMap.toFun, ← ha, (toFunLifted_factorsThrough_π f).extend_apply, toFunLifted]
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Tactic:
choose u hu using ht
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Tactic:
suffices Function.Surjective ((φ.rangeRestrict.toLinearMap).rTensor M) by
  choose p hp using this ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
  use p
  rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
    LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
  congr
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
⊢ Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
⊢ Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
Tactic:
exact rTensor_surjective M (rangeRestrict_surjective φ)
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Tactic:
choose p hp using this ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ ∃ s, (LinearMap.rTensor M φ.toLinearMap) s = t
Tactic:
use p
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✝ f : M✝ →ₚ[R✝] N
S✝ : Type v
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (LinearMap.rTensor M φ.toLinearMap) p = t
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝ f : M✝ →ₚ[R✝] N
S✝ : Type v
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (LinearMap.rTensor M φ.toLinearMap) p = t
Tactic:
rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
  LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
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✝ f : M✝ →ₚ[R✝] N
S✝ : Type v
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (LinearMap.rTensor M φ.toLinearMap) p = (LinearMap.rTensor M (φ.range.val.comp φ.rangeRestrict).toLinearMap) p
Theorem: PolynomialMap.exists_lift_of_le_rTensor_range
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✝ f : M✝ →ₚ[R✝] N
S✝ : Type v
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ S✝
R : Type u_3
inst✝⁶ : CommRing R
M : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : CommRing T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (LinearMap.rTensor M A.val.toLinearMap) u = t
this : Function.Surjective ⇑(LinearMap.rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p = (LinearMap.rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (LinearMap.rTensor M φ.toLinearMap) p = (LinearMap.rTensor M (φ.range.val.comp φ.rangeRestrict).toLinearMap) p
Tactic:
congr
Proof state after:
no goals
Theorem: PolynomialMap.π_surjective
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
⊢ Function.Surjective (PolynomialMap.π R M S)
Tactic:
intro t
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
t : S ⊗[R] M
⊢ ∃ a, PolynomialMap.π R M S a = t
Theorem: PolynomialMap.π_surjective
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
t : S ⊗[R] M
⊢ ∃ a, PolynomialMap.π R M S a = t
Tactic:
choose B hB ht using TensorProduct.Algebra.exists_of_fg t
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
⊢ ∃ a, PolynomialMap.π R M S a = t
Theorem: PolynomialMap.π_surjective
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
⊢ ∃ a, PolynomialMap.π R M S a = t
Tactic:
choose s hs using Subalgebra.FG.exists_range_eq hB
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
s : Finset S
hs : (PolynomialMap.φ R s).range = B
⊢ ∃ a, PolynomialMap.π R M S a = t
Theorem: PolynomialMap.π_surjective
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
s : Finset S
hs : (PolynomialMap.φ R s).range = B
⊢ ∃ a, PolynomialMap.π R M S a = t
Tactic:
choose p hp using exists_lift_of_le_rTensor_range M B (le_of_eq hs.symm) t ht
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
s : Finset S
hs : (PolynomialMap.φ R s).range = B
p : MvPolynomial (Fin s.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p = t
⊢ ∃ a, PolynomialMap.π R M S a = t
Theorem: PolynomialMap.π_surjective
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
t : S ⊗[R] M
B : Subalgebra R S
hB : B.FG
ht : t ∈ range (LinearMap.rTensor M B.val.toLinearMap)
s : Finset S
hs : (PolynomialMap.φ R s).range = B
p : MvPolynomial (Fin s.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p = t
⊢ ∃ a, PolynomialMap.π R M S a = t
Tactic:
exact ⟨⟨s, p⟩, hp⟩
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift
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
t : S ⊗[R] M
⊢ ∃ n ψ p, (LinearMap.rTensor M ψ.toLinearMap) p = t
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
Proof state after:
case intro.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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ ∃ n ψ p, (LinearMap.rTensor M ψ.toLinearMap) p = t
Theorem: PolynomialMap.exists_lift
Proof state before:
case intro.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
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ ∃ n ψ p, (LinearMap.rTensor M ψ.toLinearMap) p = t
Tactic:
use s.card, φ R s, p, ha
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift'
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
t : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
classical
choose A hA ht using TensorProduct.Algebra.exists_of_fg t
have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
  Subalgebra.fg_sup hA (Subalgebra.fg_adjoin_finset _)
choose gen hgen using Subalgebra.FG.exists_range_eq hB
have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
rw [← hgen] at hAB
choose p hp using exists_lift_of_le_rTensor_range M _ hAB t ht
have : s ∈ (φ R gen).range  := by
  rw [hgen]
  apply Algebra.subset_adjoin
  simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
  exact Or.inr (Algebra.subset_adjoin rfl)
choose q hq using this
use gen.card, φ R gen, p, q, hp, hq
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift'
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
t : S ⊗[R] M
s : S
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose A hA ht using TensorProduct.Algebra.exists_of_fg t
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
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
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
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have hB : Subalgebra.FG (A ⊔ Algebra.adjoin R ({s} : Finset S)) :=
  Subalgebra.fg_sup hA (Subalgebra.fg_adjoin_finset _)
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
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
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
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose gen hgen using Subalgebra.FG.exists_range_eq hB
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
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s