Theorem: PolynomialMap.π_surjective (DividedPowers/PolynomialMap/Basic.lean)

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
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

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
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

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
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

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
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

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⟩
State after:
no goals