feat(category_theory/mittag_leffler): Introduce the Mittag-Leffler co…

…ndition (#17905)

- [x] depends on: #18013



Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/category_theory/mittag_leffler.lean

@@ -0,0 +1,224 @@
+/-
+Copyright (c) 2022 Rémi Bottinelli, Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémi Bottinelli, Junyan Xu
+-/
+import category_theory.filtered
+import data.set.finite
+
+/-!
+# The Mittag-Leffler condition
+
+This files defines the Mittag-Leffler condition for cofiltered systems and (TODO) other properties
+of such systems and their sections.
+
+## Main definitions
+
+Given a functor `F : J ⥤ Type v`:
+
+* For `j : J`, `F.eventual_range j` is the intersections of all ranges of morphisms `F.map f`
+  where `f` has codomain `j`.
+* `F.is_mittag_leffler` states that the functor `F` satisfies the Mittag-Leffler
+  condition: the ranges of morphisms `F.map f` (with `f` having codomain `j`) stabilize.
+* If `J` is cofiltered `F.to_eventual_ranges` is the subfunctor of `F` obtained by restriction
+  to `F.eventual_range`.
+* `F.to_preimages` restricts a functor to preimages of a given set in some `F.obj i`. If `J` is
+  cofiltered, then it is Mittag-Leffler if `F` is, see `is_mittag_leffler.to_preimages`.
+
+## Main statements
+
+* `is_mittag_leffler_of_exists_finite_range` shows that if `J` is cofiltered and for all `j`,
+  there exists some `i` and `f : i ⟶ j` such that the range of `F.map f` is finite, then
+  `F` is Mittag-Leffler.
+* `to_eventual_ranges_surjective` shows that if `F` is Mittag-Leffler, then `F.to_eventual_ranges`
+  has all morphisms `F.map f` surjective.
+
+## Todo
+
+* Specialize to inverse systems and fintype systems.
+* Prove [Stacks: Lemma 0597](https://stacks.math.columbia.edu/tag/0597)
+
+## References
+
+* [Stacks: Mittag-Leffler systems](https://stacks.math.columbia.edu/tag/0594)
+
+## Tags
+
+Mittag-Leffler, surjective, eventual range, inverse system,
+
+-/
+
+universes u v
+
+namespace category_theory
+namespace functor
+
+open is_cofiltered set functor_to_types
+
+variables {J : Type u} [category J] (F : J ⥤ Type v) {i j k : J} (s : set (F.obj i))
+
+/--
+The eventual range of the functor `F : J ⥤ Type v` at index `j : J` is the intersection
+of the ranges of all maps `F.map f` with `i : J` and `f : i ⟶ j`.
+-/
+def eventual_range (j : J) := ⋂ i (f : i ⟶ j), range (F.map f)
+
+lemma mem_eventual_range_iff {x : F.obj j} :
+  x ∈ F.eventual_range j ↔ ∀ ⦃i⦄ (f : i ⟶ j), x ∈ range (F.map f) := mem_Inter₂
+
+/--
+The functor `F : J ⥤ Type v` satisfies the Mittag-Leffler condition if for all `j : J`,
+there exists some `i : J` and `f : i ⟶ j` such that for all `k : J` and `g : k ⟶ j`, the range
+of `F.map f` is contained in that of `F.map g`;
+in other words (see `is_mittag_leffler_iff_eventual_range`), the eventual range at `j` is attained
+by some `f : i ⟶ j`.
+-/
+def is_mittag_leffler : Prop :=
+∀ j : J, ∃ i (f : i ⟶ j), ∀ ⦃k⦄ (g : k ⟶ j), range (F.map f) ⊆ range (F.map g)
+
+lemma is_mittag_leffler_iff_eventual_range : F.is_mittag_leffler ↔
+  ∀ j : J, ∃ i (f : i ⟶ j), F.eventual_range j = range (F.map f) :=
+forall_congr $ λ j, exists₂_congr $ λ i f,
+  ⟨λ h, (Inter₂_subset _ _).antisymm $ subset_Inter₂ h, λ h, h ▸ Inter₂_subset⟩
+
+lemma is_mittag_leffler.subset_image_eventual_range (h : F.is_mittag_leffler) (f : j ⟶ i) :
+  F.eventual_range i ⊆ F.map f '' (F.eventual_range j) :=
+begin
+  obtain ⟨k, g, hg⟩ := F.is_mittag_leffler_iff_eventual_range.1 h j,
+  rw hg, intros x hx,
+  obtain ⟨x, rfl⟩ := F.mem_eventual_range_iff.1 hx (g ≫ f),
+  refine ⟨_, ⟨x, rfl⟩, by simpa only [F.map_comp]⟩,
+end
+
+lemma eventual_range_eq_range_precomp (f : i ⟶ j) (g : j ⟶ k)
+  (h : F.eventual_range k = range (F.map g)) :
+  F.eventual_range k = range (F.map $ f ≫ g) :=
+begin
+  apply subset_antisymm,
+  { apply Inter₂_subset, },
+  { rw [h, F.map_comp], apply range_comp_subset_range, }
+end
+
+lemma is_mittag_leffler_of_surjective
+  (h : ∀ (i j : J) (f : i ⟶ j), (F.map f).surjective) : F.is_mittag_leffler :=
+λ j, ⟨j, 𝟙 j, λ k g, by rw [map_id, types_id, range_id, (h k j g).range_eq]⟩
+
+/-- The subfunctor of `F` obtained by restricting to the preimages of a set `s ∈ F.obj i`. -/
+@[simps] def to_preimages : J ⥤ Type v :=
+{ obj := λ j, ⋂ f : j ⟶ i, F.map f ⁻¹' s,
+  map := λ j k g, maps_to.restrict (F.map g) _ _ $ λ x h, begin
+    rw [mem_Inter] at h ⊢, intro f,
+    rw [← mem_preimage, preimage_preimage],
+    convert h (g ≫ f), rw F.map_comp, refl,
+  end,
+  map_id' := λ j, by { simp_rw F.map_id, ext, refl },
+  map_comp' := λ j k l f g, by { simp_rw F.map_comp, refl } }
+
+variable [is_cofiltered_or_empty J]
+
+lemma eventual_range_maps_to (f : j ⟶ i) :
+  (F.eventual_range j).maps_to (F.map f) (F.eventual_range i) :=
+λ x hx, begin
+  rw mem_eventual_range_iff at hx ⊢,
+  intros k f',
+  obtain ⟨l, g, g', he⟩ := cospan f f',
+  obtain ⟨x, rfl⟩ := hx g,
+  rw [← map_comp_apply, he, F.map_comp],
+  exact ⟨_, rfl⟩,
+end
+
+lemma is_mittag_leffler.eq_image_eventual_range (h : F.is_mittag_leffler) (f : j ⟶ i) :
+  F.eventual_range i = F.map f '' (F.eventual_range j) :=
+(h.subset_image_eventual_range F f).antisymm $ maps_to'.1 (F.eventual_range_maps_to f)
+
+lemma eventual_range_eq_iff {f : i ⟶ j} :
+  F.eventual_range j = range (F.map f) ↔
+  ∀ ⦃k⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map $ g ≫ f) :=
+begin
+  rw [subset_antisymm_iff, eventual_range, and_iff_right (Inter₂_subset _ _), subset_Inter₂_iff],
+  refine ⟨λ h k g, h _ _, λ h j' f', _⟩,
+  obtain ⟨k, g, g', he⟩ := cospan f f',
+  refine (h g).trans _,
+  rw [he, F.map_comp],
+  apply range_comp_subset_range,
+end
+
+lemma is_mittag_leffler_iff_subset_range_comp : F.is_mittag_leffler ↔
+  ∀ j : J, ∃ i (f : i ⟶ j), ∀ ⦃k⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map $ g ≫ f) :=
+by simp_rw [is_mittag_leffler_iff_eventual_range, eventual_range_eq_iff]
+
+lemma is_mittag_leffler.to_preimages (h : F.is_mittag_leffler) :
+  (F.to_preimages s).is_mittag_leffler :=
+(is_mittag_leffler_iff_subset_range_comp _).2 $ λ j, begin
+  obtain ⟨j₁, g₁, f₁, -⟩ := cone_objs i j,
+  obtain ⟨j₂, f₂, h₂⟩ := F.is_mittag_leffler_iff_eventual_range.1 h j₁,
+  refine ⟨j₂, f₂ ≫ f₁, λ j₃ f₃, _⟩,
+  rintro _ ⟨⟨x, hx⟩, rfl⟩,
+  have : F.map f₂ x ∈ F.eventual_range j₁, { rw h₂, exact ⟨_, rfl⟩ },
+  obtain ⟨y, hy, h₃⟩ := h.subset_image_eventual_range F (f₃ ≫ f₂) this,
+  refine ⟨⟨y, mem_Inter.2 $ λ g₂, _⟩, subtype.ext _⟩,
+  { obtain ⟨j₄, f₄, h₄⟩ := cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁),
+    obtain ⟨y, rfl⟩ := F.mem_eventual_range_iff.1 hy f₄,
+    rw ← map_comp_apply at h₃,
+    rw [mem_preimage, ← map_comp_apply, h₄, ← category.assoc, map_comp_apply, h₃, ← map_comp_apply],
+    apply mem_Inter.1 hx },
+  { simp_rw [to_preimages_map, maps_to.coe_restrict_apply, subtype.coe_mk],
+    rw [← category.assoc, map_comp_apply, h₃, map_comp_apply] },
+end
+
+lemma is_mittag_leffler_of_exists_finite_range
+  (h : ∀ (j : J), ∃ i (f : i ⟶ j), (range $ F.map f).finite) :
+  F.is_mittag_leffler :=
+λ j, begin
+  obtain ⟨i, hi, hf⟩ := h j,
+  obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ := finset.is_well_founded_lt.wf.has_min
+    {s : finset (F.obj j) | ∃ i (f : i ⟶ j), ↑s = range (F.map f)} ⟨_, i, hi, hf.coe_to_finset⟩,
+  refine ⟨i, f, λ k g,
+    (directed_on_range.mp $ F.ranges_directed j).is_bot_of_is_min ⟨⟨i, f⟩, rfl⟩ _ _ ⟨⟨k, g⟩, rfl⟩⟩,
+  rintro _ ⟨⟨k', g'⟩, rfl⟩ hl,
+  refine (eq_of_le_of_not_lt hl _).ge,
+  have := hmin _ ⟨k', g', (m.finite_to_set.subset $ hm.substr hl).coe_to_finset⟩,
+  rwa [finset.lt_iff_ssubset, ← finset.coe_ssubset, set.finite.coe_to_finset, hm] at this,
+end
+
+/--
+The subfunctor of `F` obtained by restricting to the eventual range at each index.
+-/
+@[simps] def to_eventual_ranges : J ⥤ Type v :=
+{ obj := λ j, F.eventual_range j,
+  map := λ i j f, (F.eventual_range_maps_to f).restrict _ _ _,
+  map_id' := λ i, by { simp_rw F.map_id, ext, refl },
+  map_comp' := λ _ _ _ _ _, by { simp_rw F.map_comp, refl } }
+
+/--
+The sections of the functor `F : J ⥤ Type v` are in bijection with the sections of
+`F.eventual_ranges`.
+-/
+def to_eventual_ranges_sections_equiv : F.to_eventual_ranges.sections ≃ F.sections :=
+{ to_fun := λ s, ⟨_, λ i j f, subtype.coe_inj.2 $ s.prop f⟩,
+  inv_fun := λ s, ⟨λ j, ⟨_, mem_Inter₂.2 $ λ i f, ⟨_, s.prop f⟩⟩, λ i j f, subtype.ext $ s.prop f⟩,
+  left_inv := λ _, by { ext, refl },
+  right_inv := λ _, by { ext, refl } }
+
+/--
+If `F` satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a surjective
+functor.
+-/
+lemma surjective_to_eventual_ranges (h : F.is_mittag_leffler) (f : i ⟶ j) :
+  (F.to_eventual_ranges.map f).surjective :=
+λ ⟨x, hx⟩, by { obtain ⟨y, hy, rfl⟩ := h.subset_image_eventual_range F f hx, exact ⟨⟨y, hy⟩, rfl⟩ }
+
+/-- If `F` is nonempty at each index and Mittag-Leffler, then so is `F.to_eventual_ranges`. -/
+lemma to_eventual_ranges_nonempty (h : F.is_mittag_leffler) [∀ (j : J), nonempty (F.obj j)]
+  (j : J) : nonempty (F.to_eventual_ranges.obj j) :=
+let ⟨i, f, h⟩ := F.is_mittag_leffler_iff_eventual_range.1 h j in
+by { rw [to_eventual_ranges_obj, h], apply_instance }
+
+/-- If `F` has all arrows surjective, then it "factors through a poset". -/
+lemma thin_diagram_of_surjective (Fsur : ∀ (i j : J) (f : i ⟶ j), (F.map f).surjective)
+  (i j) (f g : i ⟶ j) : F.map f = F.map g :=
+let ⟨k, φ, hφ⟩ := cone_maps f g in
+(Fsur k i φ).injective_comp_right $ by simp_rw [← types_comp, ← F.map_comp, hφ]
+
+end functor
+end category_theory

src/order/directed.lean

@@ -46,6 +46,10 @@ by simp [directed, directed_on]; refine ball_congr (λ x hx, by simp; refl)
 
 alias directed_on_iff_directed ↔ directed_on.directed_coe _
 
+theorem directed_on_range {f : β → α} :
+  directed r f ↔ directed_on r (set.range f) :=
+by simp_rw [directed, directed_on, set.forall_range_iff, set.exists_range_iff]
+
 theorem directed_on_image {s} {f : β → α} :
   directed_on r (f '' s) ↔ directed_on (f ⁻¹'o r) s :=
 by simp only [directed_on, set.ball_image_iff, set.bex_image_iff, order.preimage]
@@ -166,6 +170,14 @@ protected lemma is_min.is_bot [is_directed α (≥)] (h : is_min a) : is_bot a :
 protected lemma is_max.is_top [is_directed α (≤)] (h : is_max a) : is_top a :=
 h.to_dual.is_bot
 
+lemma directed_on.is_bot_of_is_min {s : set α} (hd : directed_on (≥) s)
+  {m} (hm : m ∈ s) (hmin : ∀ a ∈ s, a ≤ m → m ≤ a) : ∀ a ∈ s, m ≤ a :=
+λ a as, let ⟨x, xs, xm, xa⟩ := hd m hm a as in (hmin x xs xm).trans xa
+
+lemma directed_on.is_top_of_is_max {s : set α} (hd : directed_on (≤) s)
+  {m} (hm : m ∈ s) (hmax : ∀ a ∈ s, m ≤ a → a ≤ m) : ∀ a ∈ s, a ≤ m :=
+@directed_on.is_bot_of_is_min αᵒᵈ _ s hd m hm hmax
+
 lemma is_top_or_exists_gt [is_directed α (≤)] (a : α) : is_top a ∨ (∃ b, a < b) :=
 (em (is_max a)).imp is_max.is_top not_is_max_iff.mp