Semistable res iff semistable quot
HarderNarasimhan.impl.semistable_res_iff_semistable_quot
Project documentation
Semistability of a restriction vs. semistability on the quotient lattice. This lemma is the key “translation” step for coprimary filtrations: * restricting the slope μ R M to an interval (N₁, N₂) corresponds to * the induced slope on the submodule lattice of the quotient module N₂ / N₁. The statement is phrased as an equivalence between `Semistable...
Exact Lean statement
lemma semistable_res_iff_semistable_quot {R : Type*} [CommRing R] [IsNoetherianRing R]
{M : Type*} [Nontrivial M] [AddCommGroup M] [Module R M] [Module.Finite R M]
(N₁ N₂ : ℒ R M) (hN : N₁ < N₂) :
Semistable (Resμ ⟨(N₁, N₂), hN⟩ (μ R M)) ↔
@Semistable (@ℒ R _ _ (↥N₂ ⧸ N₁.submoduleOf N₂) (@quot_ntl R _ _ M _ _ _ _ N₁ N₂ hN)
_ _ _) (@quot_ntl' R _ _ M _ _ _ _ N₁ N₂ hN) _ _ (S R) _
(@μ R _ _ (↥N₂ ⧸ Submodule.submoduleOf N₁ N₂)
(@quot_ntl R _ _ M _ _ _ _ N₁ N₂ hN) _ _ _)Formal artifact
Lean source
lemma semistable_res_iff_semistable_quot {R : Type*} [CommRing R] [IsNoetherianRing R]{M : Type*} [Nontrivial M] [AddCommGroup M] [Module R M] [Module.Finite R M] (N₁ N₂ : ℒ R M) (hN : N₁ < N₂) : Semistable (Resμ ⟨(N₁, N₂), hN⟩ (μ R M)) ↔ @Semistable (@ℒ R _ _ (↥N₂ ⧸ N₁.submoduleOf N₂) (@quot_ntl R _ _ M _ _ _ _ N₁ N₂ hN) _ _ _) (@quot_ntl' R _ _ M _ _ _ _ N₁ N₂ hN) _ _ (S R) _ (@μ R _ _ (↥N₂ ⧸ Submodule.submoduleOf N₁ N₂) (@quot_ntl R _ _ M _ _ _ _ N₁ N₂ hN) _ _ _) := by refine ⟨?_, ?_⟩ · intro h letI : Nontrivial (↥N₂ ⧸ N₁.submoduleOf N₂) := quot_ntl hN letI : Nontrivial (ℒ R (↥N₂ ⧸ N₁.submoduleOf N₂)) := quot_ntl' hN refine { semistable := ?_ } intro X hX have hres := h.semistable ⟨lift_quot N₁ N₂ X, lift_quot_middle N₁ N₂ (le_of_lt hN) X⟩ (fun hc ↦ lift_quot_not_bot N₁ N₂ X hX (Subtype.coe_inj.mpr hc)) have hmid := lift_quot_middle N₁ N₂ (le_of_lt hN) X have hneq : lift_quot N₁ N₂ X ≠ N₁ := lift_quot_not_bot N₁ N₂ X hX have hres' : ¬ μA (μ R M) ⟨(N₁, lift_quot N₁ N₂ X), lt_of_le_of_ne hmid.1 hneq.symm⟩ > μA (μ R M) ⟨(N₁, N₂), hN⟩ := by have := hres simp only [μA_res_intvl] at this exact this rw [muA_eq_quot_muA hmid.1 hmid.2 hneq, muA_eq_quot_muA (le_of_lt hN) le_rfl hN.ne.symm] at hres' simpa [lift_quot, Submodule.comap_map_eq, Submodule.ker_subtype, Submodule.map_comap_eq_self, Submodule.range_mkQ] using hres' · intro h letI : Nontrivial (↥N₂ ⧸ N₁.submoduleOf N₂) := quot_ntl hN letI : Nontrivial (ℒ R (↥N₂ ⧸ N₁.submoduleOf N₂)) := quot_ntl' hN refine { semistable := ?_ } intro W hW have hW' : W.val ≠ N₁ := fun hEq ↦ hW (Subtype.ext hEq) have hquot := h.semistable (Submodule.map (N₁.submoduleOf N₂).mkQ (Submodule.comap N₂.subtype W.val)) (map_comap_ne_bot W.prop.1 W.prop.2 hW') have hquot' : ¬ μA (μ R M) ⟨(N₁, W.val), lt_of_le_of_ne W.prop.1 hW'.symm⟩ > μA (μ R M) ⟨(N₁, N₂), hN⟩ := by simpa [muA_eq_quot_muA (N₁ := N₁) (N₂ := N₂) (W := W.val) W.prop.1 W.prop.2 hW', muA_eq_quot_muA (N₁ := N₁) (N₂ := N₂) (W := N₂) (le_of_lt hN) le_rfl hN.ne.symm, Submodule.comap_top, Submodule.map_top, Submodule.range_mkQ] using hquot have hWne : (⊥ : Interval ⟨(N₁, N₂), hN⟩) ≠ W := fun hEq ↦ hW' (congrArg Subtype.val hEq).symm have : ¬ μA (Resμ ⟨(N₁, N₂), hN⟩ (μ R M)) ⟨(⊥, W), lt_of_le_of_ne W.prop.1 hWne⟩ > μA (Resμ ⟨(N₁, N₂), hN⟩ (μ R M)) ⟨(⊥, ⊤), bot_lt_top⟩ := by simp only [μA_res_intvl] exact hquot' exact this- Project
- Harder-Narasimhan
- License
- Apache-2.0
- Commit
- 20220e90b72c
- Source
- HarderNarasimhan/CoprimaryFiltration/Impl.lean:963-1015
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Associated Primes ker mk Linear Map eq
HarderNarasimhan.CommutativeAlgebra.associatedPrimes_ker_mkLinearMap_eq
Project documentation
Associated primes of the kernel of the localization map. This identifies the associated primes of ker (LocalizedModule.mkLinearMap S M) : Submodule R M with the associated primes of M that do meet the multiplicative set S. Equivalently, these are the associated primes of M after removing those disjoint from S. This lemma is used as the “kernel...
Source project: Harder-Narasimhan
Person-level attribution pending.
Associated Primes ker mk Linear Map subset
HarderNarasimhan.CommutativeAlgebra.associatedPrimes_ker_mkLinearMap_subset
Plain-language statement
One-sided inclusion for associated primes of the kernel of the localization map. If p ∈ associatedPrimes R (ker (mkLinearMap S M)), then p is an associated prime of M and p is not disjoint from the multiplicative set S. This is one direction of associatedPrimes_ker_mkLinearMap_eq.
Source project: Harder-Narasimhan
Person-level attribution pending.
Associated Primes localized Module subset disjoint
HarderNarasimhan.CommutativeAlgebra.associatedPrimes_localizedModule_subset_disjoint
Plain-language statement
Associated primes of a localized module are disjoint from the multiplicative set. More precisely, if p ∈ associatedPrimes R (LocalizedModule S M), then p.carrier ∩ S = ∅. This is a standard fact in commutative algebra: an element of S becomes a unit after localization, so no associated prime of the localized module can contain an element of S.
Source project: Harder-Narasimhan
Person-level attribution pending.