R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
⊢ Submodule.FG s
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
⊢ IsNoetherian R { x // x ∈ N } ↔ ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
refine ⟨fun ⟨hn⟩ => fun s hs =>
  have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
  Submodule.map_comap_eq_self this ▸ (hn _).map _,
  fun h => ⟨fun s => ?_⟩⟩
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
⊢ Submodule.FG s
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
⊢ Submodule.FG s
have f := (Submodule.equivMapOfInjective N.subtype Subtype.val_injective s).symm
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
⊢ Submodule.FG s
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
⊢ Submodule.FG s
have h₁ := h (s.map N.subtype) (Submodule.map_subtype_le N s)
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
⊢ Submodule.FG s
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
⊢ Submodule.FG s
have h₂ : (⊤ : Submodule R (s.map N.subtype)).map f = ⊤ := by simp
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
h₃ : Submodule.FG (Submodule.map ↑f ⊤)
⊢ Submodule.FG s
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
⊢ Submodule.FG s
have h₃ := ((Submodule.fg_top _).2 h₁).map (↑f : _ →ₗ[R] s)
no goals
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
h₂ : Submodule.map f ⊤ = ⊤
h₃ : Submodule.FG (Submodule.map ↑f ⊤)
⊢ Submodule.FG s
exact (Submodule.fg_top _).1 (h₂ ▸ h₃)
no goals
R : Type u_1
M : Type u_2
P : Type ?u.632
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid P
inst✝¹ : Module R M
inst✝ : Module R P
N : Submodule R M
h : ∀ (s : Submodule R M), s ≤ N → Submodule.FG s
s : Submodule R { x // x ∈ N }
f : { x // x ∈ Submodule.map (Submodule.subtype N) s } ≃ₗ[R] { x // x ∈ s }
h₁ : Submodule.FG (Submodule.map (Submodule.subtype N) s)
⊢ Submodule.map f ⊤ = ⊤
simp