FiniteFiberBranches.lean

1 import PaperX.Compactness
2 import Mathlib.Data.Fintype.EquivFin
3 import Mathlib.Data.Fintype.Sigma
4 import Mathlib.Basic.Finite.Sigma
5 import Mathlib.Logic.Equiv.Sum
6 
7 /-!
8 Lifting compatible classes to compatible representatives using finite fibers.
9 The fibers above a fixed quotient branch form their own inverse system.
10 Surjectivity of its transition maps is neither required nor asserted.
11 -/
12 set_option autoImplicit false
13 
14 namespace PaperX.FiniteFiberBranches
15 open PaperX.Compactness
16 
17 /-- A map of towers commutes with each immediate reduction. -/
18 structure TowerMap (T Q : Tower) where
19   map : (k : ℕ) → T.Level k → Q.Level k
20   parent_commutes : ∀ k x,
21     map k (T.parent k x) = Q.parent k (map (k + 1) x)
22 
23 variable {T Q : Tower}
24 
25 /-- A tower map sends actual compatible representatives to compatible classes. -/
26 def mapBranch (f : TowerMap T Q) (b : Branch T) : Branch Q where
27   value k := f.map k (b.value k)
28   compatible k := by
29     rw [← f.parent_commutes, b.compatible]
30 
31 /-- The fiber above each member of a fixed compatible class branch. -/
32 def fiberTower (f : TowerMap T Q) (b : Branch Q) : Tower where
33   Level k := {x : T.Level k // f.map k x = b.value k}
34   parent k x := ⟨T.parent k x.val, by
35     rw [f.parent_commutes, x.property, b.compatible]⟩
36 
37 /-- Type-theoretic finiteness gives the complete finite lists required by the
38 elementary compactness theorem. -/
39 theorem finite_levels (S : Tower) (h : ∀ k, Finite (S.Level k)) :
40     FiniteLevels S := by
41   intro k
42   let : Finite (S.Level k) := h k
43   let : Fintype (S.Level k) := Fintype.ofFinite _
44   classical
45   exact ⟨Finset.univ.toList, by simp⟩
46 
47 /-- A fixed compatible class branch has an exactly compatible representative
48 branch if its fibers are finite and nonempty. The full quotient levels may be
49 infinite, and no reduction map is assumed surjective. -/
50 theorem lift_branch_of_fibers (f : TowerMap T Q) (b : Branch Q)
51     (finite : ∀ k, Finite {x : T.Level k // f.map k x = b.value k})
52     (occupied : ∀ k, ∃ x, f.map k x = b.value k) :
53     ∃ a : Branch T, ∀ k, f.map k (a.value k) = b.value k := by
54   obtain ⟨c⟩ := finite_branch_compactness (fiberTower f b)
55     (finite_levels _ finite)
56     (fun k => let ⟨x, hx⟩ := occupied k; ⟨x, hx⟩)
57   let a : Branch T := {
58     value k := (c.value k).val
59     compatible k := congrArg Subtype.val (c.compatible k)
60   }
61   exact ⟨a, fun k => (c.value k).property⟩
62 
63 /-- Levelwise surjective quotient maps with finite fibers lift every quotient
64 branch, without assuming surjectivity for the parent maps. -/
65 theorem lift_branch (f : TowerMap T Q)
66     (surjective : ∀ k, Function.Surjective (f.map k))
67     (finite : ∀ k y, Finite {x : T.Level k // f.map k x = y})
68     (b : Branch Q) :
69     ∃ a : Branch T, ∀ k, f.map k (a.value k) = b.value k :=
70   lift_branch_of_fibers f b (fun k => finite k (b.value k))
71     (fun k => surjective k (b.value k))
72 
73 /-- A finite codomain and finite fibers imply a finite domain. Surjectivity is
74 not needed here: the disjoint union of the fibers already enumerates it. -/
75 theorem finite_of_fibers {A B : Type*} (f : A → B) [Finite B]
76     (finite : ∀ y, Finite {x : A // f x = y}) : Finite A := by
77   let : ∀ y, Finite {x : A // f x = y} := finite
78   exact Finite.of_equiv _ (Equiv.sigmaFiberEquiv f)
79 
80 /-- Finitely many classes, each with finitely many representatives, give a
81 finite actual level. This does not infer finiteness from coefficient rings alone. -/
82 theorem finite_domain_levels (f : TowerMap T Q)
83     (classes : ∀ k, Finite (Q.Level k))
84     (fibers : ∀ k y, Finite {x : T.Level k // f.map k x = y}) :
85     ∀ k, Finite (T.Level k) := by
86   intro k
87   let : Finite (Q.Level k) := classes k
88   exact finite_of_fibers (f.map k) (fibers k)
89 
90 end PaperX.FiniteFiberBranches

Back to source controls