CompositionSiteExamples.lean

1 import KomorebiSpace.CompositionStack
2 import Mathlib.Tactic.FinCases
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The composition topology is not merely object or arrow coverage
8 
9 Proper patches of a four-view chain can cover all compositions. In a
10 three-view chain, proper patches cover all individual arrows but can omit
11 one composition. These examples test the specified covering doctrine.
12 -/
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace CompositionSiteExamples
16 
17 /-- Delete one of the views, retaining the induced full patch. -/
18 def omitOne (n : ℕ) (i : Fin n) : Set (Fin n) := {x | x ≠ i}
19 
20 /-- Four proper patches cover every composable pair in the four-view chain. -/
21 theorem four_proper_cover : CompositionSite.FamilyCovers
22     (Set.univ : Set (Fin 4)) (omitOne 4) := by
23   intro q _
24   have he : ∀ a b c : Fin 4, ∃ i : Fin 4, a ≠ i ∧ b ≠ i ∧ c ≠ i := by decide
25   obtain ⟨i, ha, hb, hc⟩ := he q.a q.b q.c
26   exact ⟨i, (q.support_le_iff _).mpr ⟨ha, hb, hc⟩⟩
27 
28 /-- None of the four patches is the global patch. -/
29 theorem four_patches_proper (i : Fin 4) : omitOne 4 i ≠ Set.univ := by
30   intro h
31   have hi : i ∈ omitOne 4 i := by rw [h]; trivial
32   exact hi rfl
33 
34 /-- Their generated sieve really belongs to the constructed Grothendieck topology. -/
35 theorem four_sieve_covering :
36     Sieve.ofArrows (omitOne 4) (fun i => homOfLE (Set.subset_univ (omitOne 4 i))) ∈
37       CompositionSite.topology (Fin 4) Set.univ := by
38   rw [CompositionSite.ofArrows_covering_iff]
39   exact four_proper_cover
40 
41 /-- In three views, every individual arrow is still contained in a proper patch. -/
42 theorem three_cover_arrows : ViewSystem.TransitionCover (omitOne 3) := by
43   intro a b _
44   have he : ∃ i : Fin 3, a ≠ i ∧ b ≠ i := by
45     fin_cases a <;> fin_cases b <;> decide
46   exact he
47 
48 /-- But the composition 0 to 1 to 2 is absent from every such patch. -/
49 theorem three_not_composition_cover : ¬ CompositionSite.FamilyCovers
50     (Set.univ : Set (Fin 3)) (omitOne 3) := by
51   intro h
52   let q : CompositionSite.Triangle (Fin 3) :=
53     ⟨0, 1, 2, homOfLE (by decide), homOfLE (by decide)⟩
54   obtain ⟨i, hi⟩ := h q (Set.subset_univ _)
55   have ha := hi q.a_mem
56   have hb := hi q.b_mem
57   have hc := hi q.c_mem
58   fin_cases i
59   · exact ha rfl
60   · exact hb rfl
61   · exact hc rfl
62 
63 /-- Object and arrow coverage cannot replace composition coverage in this site. -/
64 theorem three_sieve_not_covering :
65     Sieve.ofArrows (omitOne 3) (fun i => homOfLE (Set.subset_univ (omitOne 3 i))) ∉
66       CompositionSite.topology (Fin 3) Set.univ := by
67   rw [CompositionSite.ofArrows_covering_iff]
68   exact three_not_composition_cover
69 
70 end CompositionSiteExamples
71 end KomorebiSpace

Back to source controls