Theorem: PolynomialMap.exists_lift_of_le_rTensor_range (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✝
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
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

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

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

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

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

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

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