Plain-language statement
Proposition 3.8 (part 1): totality on StI μ I under comparability/attainment hypotheses. Under convexity and well-foundedness, if either: - the target S is totally ordered, or - all relevant μA infima are attained, then the order on the set of stable breakpoints becomes total. API note: this produces an instance of Std.Total for the subtype `StI μ...
Exact Lean statement
lemma prop3d8₁ {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]
{S : Type*} [CompleteLattice S]
(μ : {p :ℒ × ℒ // p.1 < p.2} → S)-- (hμ : μDCC μ)
(I : {p : ℒ × ℒ // p.1 < p.2}) (hμcvx : ConvexI I μ)
(h : (@Std.Total S (· ≤ ·)) ∨
∀ z : ℒ, (hzI : InIntvl I z) → (hz : I.val.1 ≠ z) →
IsAttained μ ⟨(I.val.1 , z) , lt_of_le_of_ne hzI.left hz⟩) :
@Std.Total (StI μ I) (· ≤ ·)Formal artifact
Lean source
lemma prop3d8₁ {ℒ : Type*} [Nontrivial ℒ] [Lattice ℒ] [BoundedOrder ℒ] [WellFoundedGT ℒ]{S : Type*} [CompleteLattice S](μ : {p :ℒ × ℒ // p.1 < p.2} → S)-- (hμ : μDCC μ)(I : {p : ℒ × ℒ // p.1 < p.2}) (hμcvx : ConvexI I μ)(h : (@Std.Total S (· ≤ ·)) ∨ ∀ z : ℒ, (hzI : InIntvl I z) → (hz : I.val.1 ≠ z) → IsAttained μ ⟨(I.val.1 , z) , lt_of_le_of_ne hzI.left hz⟩) :@Std.Total (StI μ I) (· ≤ ·) := by refine { total := ?_ } rintro ⟨x,hx⟩ ⟨x',hx'⟩ have h₁ : IsComparable (μA μ ⟨(I.val.1,x),lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose⟩) (μA μ ⟨(I.val.1,x'),lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose⟩) ∨ IsAttained μ ⟨(I.val.1 , x ⊔ x') , lt_sup_of_lt_right <| lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose⟩:= by rcases h with htotal | hattained · exact Or.inl <| htotal.total (μA μ ⟨(I.val.1,x),lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose⟩) (μA μ ⟨(I.val.1,x'),lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose⟩) · exact Or.inr <| hattained (x ⊔ x') ⟨le_sup_of_le_left hx.out.choose.1,sup_le hx.out.choose.2 hx'.out.choose.2⟩ <| ne_of_lt <| lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose have h₂ : μA μ ⟨(I.val.1, x), lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose⟩ = μA μ ⟨(I.val.1, x ⊔ x'), lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose⟩ ∨ μA μ ⟨(I.val.1, x'), lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose⟩ = μA μ ⟨(I.val.1, x ⊔ x'), lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose⟩ := by rcases (impl.prop2d8₂I I μ hμcvx x hx.out.choose x' hx'.out.choose I.val.1 ⟨le_rfl,le_of_lt I.prop⟩ ⟨lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose, lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose⟩ h₁) with c1 | c2 · exact Or.inl <| eq_of_le_of_not_lt c1 <| hx.out.choose_spec.choose_spec.1 (x ⊔ x') ⟨le_sup_of_le_left hx.out.choose.1,sup_le hx.out.choose.2 hx'.out.choose.2⟩ <| ne_of_lt <| lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose · exact Or.inr <| eq_of_le_of_not_lt c2 <| hx'.out.choose_spec.choose_spec.1 (x ⊔ x') ⟨le_sup_of_le_left hx.out.choose.1,sup_le hx.out.choose.2 hx'.out.choose.2⟩ <| ne_of_lt <| lt_sup_of_lt_right <| lt_of_le_of_ne hx'.out.choose.1 hx'.out.choose_spec.choose have h₃ : x ⊔ x' ≤ x ∨ x ⊔ x' ≤ x' := by rcases h₂ with c1 | c2 · exact Or.inl <| hx.out.choose_spec.choose_spec.2 (x ⊔ x') ⟨le_sup_of_le_left hx.out.choose.1, sup_le hx.out.choose.2 hx'.out.choose.2⟩ (ne_of_lt <| lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose) c1.symm · exact Or.inr <| hx'.out.choose_spec.choose_spec.2 (x ⊔ x') ⟨le_sup_of_le_left hx.out.choose.1, sup_le hx.out.choose.2 hx'.out.choose.2⟩ (ne_of_lt <| lt_sup_of_lt_left <| lt_of_le_of_ne hx.out.choose.1 hx.out.choose_spec.choose) c2.symm rcases h₃ with c1 | c2 · exact Or.inr (sup_le_iff.1 c1).2 · exact Or.inl (sup_le_iff.1 c2).1- Project
- Harder-Narasimhan
- License
- Apache-2.0
- Commit
- 20220e90b72c
- Source
- HarderNarasimhan/Semistability/Impl.lean:549-594
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.