Theorem: TensorProduct.Algebra.exists_of_fg (DividedPowers/ForMathlib/DirectLimit.lean)

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
t : S ⊗[R] N
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
let ⟨P, hP, ht⟩ := TensorProduct.exists_of_fg t
State after:
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
t : S ⊗[R] N
P : Submodule R S
hP : P.FG
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)

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
t : S ⊗[R] N
P : Submodule R S
hP : P.FG
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
obtain ⟨s, hs⟩ := hP
State after:
case intro
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)

State before:
case intro
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ∃ A, A.FG ∧ t ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)
Tactic:
use Algebra.adjoin R s, Subalgebra.fg_adjoin_finset _
State after:
case right
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)

State before:
case right
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
have : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R (s : Set S)) := by
  simp only [← hs, Submodule.span_le, Subalgebra.coe_toSubmodule]
  exact Algebra.subset_adjoin
State after:
case right
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)

State before:
case right
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
rw [← Submodule.subtype_comp_inclusion P _ this,
  LinearMap.rTensor_comp] at ht
State after:
case right
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
t : S ⊗[R] N
P : Submodule R S
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
ht :
  t ∈
    LinearMap.range
      (LinearMap.rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ
        LinearMap.rTensor N (Submodule.inclusion this))
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)

State before:
case right
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
t : S ⊗[R] N
P : Submodule R S
s : Finset S
hs : Submodule.span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
ht :
  t ∈
    LinearMap.range
      (LinearMap.rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ
        LinearMap.rTensor N (Submodule.inclusion this))
⊢ t ∈ LinearMap.range (LinearMap.rTensor N (Algebra.adjoin R ↑s).val.toLinearMap)
Tactic:
exact LinearMap.range_comp_le_range _ _ ht
State after:
no goals

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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
Tactic:
simp only [← hs, Submodule.span_le, Subalgebra.coe_toSubmodule]
State after:
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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑s)

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
t : S ⊗[R] N
P : Submodule R S
ht : t ∈ LinearMap.range (LinearMap.rTensor N P.subtype)
s : Finset S
hs : Submodule.span R ↑s = P
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑s)
Tactic:
exact Algebra.subset_adjoin
State after:
no goals