Theorem: TensorProduct.Algebra.eq_of_fg_of_subtype_eq
Proof state before:
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j') u'
hu'₁ : u'₁ = (LinearMap.rTensor N j') u'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
⊢ (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j'
Tactic:
ext
Proof state after:
case h.a
R : Type u_1
S : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (LinearMap.rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (LinearMap.rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j) u
hu₁ : u₁ = (LinearMap.rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (LinearMap.rTensor N j') u'
hu'₁ : u'₁ = (LinearMap.rTensor N j') u'
this : (LinearMap.rTensor N P₁.subtype) u₁ = (LinearMap.rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u₁ = (LinearMap.rTensor N (Submodule.inclusion hP₁_le)) u'₁
s : Finset S
hs : Submodule.span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j
x✝ : ↥P'
⊢ ↑(((Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype) x✝) =
    ↑((Submodule.inclusion hP'₁_le ∘ₗ Submodule.inclusion hP₁_le ∘ₗ j') x✝)