feat: cardinalities in specific inverse systems (#18067)

We compute the cardinality of each node in an inverse system `F i` indexed by a well-order in which every map between successive nodes has constant fiber `X i`, and every limit node is the `limit` of the inverse subsystem formed by all previous nodes. (To avoid importing `Cardinal`, we in fact construct a bijection rather than stating the result in terms of `Cardinal.mk`.)



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Author: alreadydone

Mathlib.lean

@@ -3784,6 +3784,7 @@ import Mathlib.Order.CountableDenseLinearOrder
 import Mathlib.Order.Cover
 import Mathlib.Order.Defs
 import Mathlib.Order.Directed
+import Mathlib.Order.DirectedInverseSystem
 import Mathlib.Order.Disjoint
 import Mathlib.Order.Disjointed
 import Mathlib.Order.Estimator

Mathlib/Algebra/DirectLimit.lean

@@ -9,6 +9,7 @@ import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.Order.DirectedInverseSystem
 import Mathlib.Tactic.SuppressCompilation
 
 /-!
@@ -43,24 +44,6 @@ variable {ι : Type v}
 variable [Preorder ι]
 variable (G : ι → Type w)
 
-/-- A directed system is a functor from a category (directed poset) to another category. -/
-class DirectedSystem (f : ∀ i j, i ≤ j → G i → G j) : Prop where
-  map_self' : ∀ i x h, f i i h x = x
-  map_map' : ∀ {i j k} (hij hjk x), f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x
-
-section
-
-variable {G}
-variable (f : ∀ i j, i ≤ j → G i → G j) [DirectedSystem G fun i j h => f i j h]
-
-theorem DirectedSystem.map_self i x h : f i i h x = x :=
-  DirectedSystem.map_self' i x h
-theorem DirectedSystem.map_map {i j k} (hij hjk x) :
-    f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x :=
-  DirectedSystem.map_map' hij hjk x
-
-end
-
 namespace Module
 
 variable [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
@@ -71,13 +54,13 @@ variable (f : ∀ i j, i ≤ j → G i →ₗ[R] G j)
 `fun i j h ↦ f i j h` can confuse the simplifier. -/
 nonrec theorem DirectedSystem.map_self [DirectedSystem G fun i j h => f i j h] (i x h) :
     f i i h x = x :=
-  DirectedSystem.map_self (fun i j h => f i j h) i x h
+  DirectedSystem.map_self (f := (f · · ·)) x
 
 /-- A copy of `DirectedSystem.map_map` specialized to linear maps, as otherwise the
 `fun i j h ↦ f i j h` can confuse the simplifier. -/
 nonrec theorem DirectedSystem.map_map [DirectedSystem G fun i j h => f i j h] {i j k} (hij hjk x) :
     f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x :=
-  DirectedSystem.map_map (fun i j h => f i j h) hij hjk x
+  DirectedSystem.map_map (f := (f · · ·)) hij hjk x
 
 variable (G)
 
@@ -649,7 +632,7 @@ theorem of.zero_exact_aux2 {x : FreeCommRing (Σi, G i)} {s t} [DecidablePred (
       restriction_of, dif_pos (hst hps), lift_of]
     dsimp only
     -- Porting note: Lean 3 could get away with far fewer hints for inputs in the line below
-    have := DirectedSystem.map_map (fun i j h => f' i j h) (hj p hps) hjk
+    have := DirectedSystem.map_map (f := (f' · · ·)) (hj p hps) hjk
     rw [this]
   · rintro x y ihx ihy
     rw [(restriction _).map_add, (FreeCommRing.lift _).map_add, (f' j k hjk).map_add, ihx, ihy,
@@ -678,7 +661,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
           restriction_of, dif_pos, lift_of, lift_of]
         on_goal 1 =>
           dsimp only
-          have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j)
+          have := DirectedSystem.map_map (f := (f' · · ·)) hij le_rfl
           rw [this]
           · exact sub_self _
         exacts [Or.inl rfl, Or.inr rfl]

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -245,7 +245,7 @@ theorem Step.isIntegral (n) : ∀ z : Step k n, IsIntegral k z := by
     · convert h -- Porting note: This times out at 500000
 
 instance toStepOfLE.directedSystem : DirectedSystem (Step k) fun i j h => toStepOfLE k i j h :=
-  ⟨fun _ x _ => Nat.leRecOn_self x, fun h₁₂ h₂₃ x => (Nat.leRecOn_trans h₁₂ h₂₃ x).symm⟩
+  ⟨fun _ => Nat.leRecOn_self, fun _ _ _ h₁₂ h₂₃ x => (Nat.leRecOn_trans h₁₂ h₂₃ x).symm⟩
 
 end AlgebraicClosure
 

Mathlib/Logic/Equiv/Basic.lean

@@ -1717,6 +1717,14 @@ theorem piCongr'_symm_apply_symm_apply (f : ∀ b, Z b) (b : β) :
 
 end
 
+/-- Transport dependent functions through an equality of sets. -/
+@[simps!] def piCongrSet {α} {W : α → Sort w} {s t : Set α} (h : s = t) :
+    (∀ i : {i // i ∈ s}, W i) ≃ (∀ i : {i // i ∈ t}, W i) where
+  toFun f i := f ⟨i, h ▸ i.2⟩
+  invFun f i := f ⟨i, h.symm ▸ i.2⟩
+  left_inv f := rfl
+  right_inv f := rfl
+
 section BinaryOp
 
 variable {α₁ β₁ : Type*} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁)

Mathlib/ModelTheory/DirectLimit.lean

@@ -3,11 +3,11 @@ Copyright (c) 2022 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Gabin Kolly
 -/
+import Mathlib.Data.Finite.Sum
 import Mathlib.Data.Fintype.Order
-import Mathlib.Algebra.DirectLimit
-import Mathlib.ModelTheory.Quotients
 import Mathlib.ModelTheory.FinitelyGenerated
-import Mathlib.Data.Finite.Sum
+import Mathlib.ModelTheory.Quotients
+import Mathlib.Order.DirectedInverseSystem
 
 /-!
 # Direct Limits of First-Order Structures
@@ -45,13 +45,13 @@ namespace DirectedSystem
 /-- A copy of `DirectedSystem.map_self` specialized to `L`-embeddings, as otherwise the
 `fun i j h ↦ f i j h` can confuse the simplifier. -/
 nonrec theorem map_self [DirectedSystem G fun i j h => f i j h] (i x h) : f i i h x = x :=
-  DirectedSystem.map_self (fun i j h => f i j h) i x h
+  DirectedSystem.map_self (f := (f · · ·)) x
 
 /-- A copy of `DirectedSystem.map_map` specialized to `L`-embeddings, as otherwise the
 `fun i j h ↦ f i j h` can confuse the simplifier. -/
 nonrec theorem map_map [DirectedSystem G fun i j h => f i j h] {i j k} (hij hjk x) :
     f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x :=
-  DirectedSystem.map_map (fun i j h => f i j h) hij hjk x
+  DirectedSystem.map_map (f := (f · · ·)) hij hjk x
 
 variable {G' : ℕ → Type w} [∀ i, L.Structure (G' i)] (f' : ∀ n : ℕ, G' n ↪[L] G' (n + 1))
 
@@ -73,8 +73,8 @@ theorem coe_natLERec (m n : ℕ) (h : m ≤ n) :
       Embedding.comp_apply, ih]
 
 instance natLERec.directedSystem : DirectedSystem G' fun i j h => natLERec f' i j h :=
-  ⟨fun _ _ _ => congr (congr rfl (Nat.leRecOn_self _)) rfl,
-   fun hij hjk => by simp [Nat.leRecOn_trans hij hjk]⟩
+  ⟨fun _ _ => congr (congr rfl (Nat.leRecOn_self _)) rfl,
+   fun _ _ _ hij hjk => by simp [Nat.leRecOn_trans hij hjk]⟩
 
 end DirectedSystem
 
@@ -444,8 +444,8 @@ variable [Nonempty ι] [IsDirected ι (· ≤ ·)]
 variable {M N : Type*} [L.Structure M] [L.Structure N] (S : ι →o L.Substructure M)
 
 instance : DirectedSystem (fun i ↦ S i) (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) where
-  map_self' := fun _ _ _ ↦ rfl
-  map_map' := fun _ _ _ ↦ rfl
+  map_self _ _ := rfl
+  map_map _ _ _ _ _ _ := rfl
 
 namespace DirectLimit
 

Mathlib/ModelTheory/PartialEquiv.lean

@@ -303,13 +303,13 @@ variable (S : ι →o M ≃ₚ[L] N)
 
 instance : DirectedSystem (fun i ↦ (S i).dom)
     (fun _ _ h ↦ Substructure.inclusion (dom_le_dom (S.monotone h))) where
-  map_self' := fun _ _ _ ↦ rfl
-  map_map' := fun _ _ _ ↦ rfl
+  map_self _ _ := rfl
+  map_map _ _ _ _ _ _ := rfl
 
 instance : DirectedSystem (fun i ↦ (S i).cod)
     (fun _ _ h ↦ Substructure.inclusion (cod_le_cod (S.monotone h))) where
-  map_self' := fun _ _ _ ↦ rfl
-  map_map' := fun _ _ _ ↦ rfl
+  map_self _ _ := rfl
+  map_map _ _ _ _ _ _ := rfl
 
 /-- The limit of a directed system of PartialEquivs. -/
 noncomputable def partialEquivLimit : M ≃ₚ[L] N where