English
Pairwise-to-LeCover diagram is aligned through a chain of isomorphisms of cones.
Русский
Диаграмма от парных к OpensLeCover выравнивается через цепочку изоморфизмов конусов.
LaTeX
$$$\text{pairwiseCoconeIso} : (Pairwise.cocone U)^{op} \cong ((opensLeCoverCocone U)^{op} \circ (pairwiseToOpensLeCover U)^{op})$$$
Lean4
/-- The diagram consisting of the `U i` and `U i ⊓ U j` is cofinal in the diagram
of all opens contained in some `U i`.
-/
instance : Functor.Final (pairwiseToOpensLeCover U) :=
⟨fun V =>
isConnected_of_zigzag fun A B =>
by
rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩ | ⟨i, j⟩, a⟩ <;> rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩
· refine
⟨[{ left := ⟨⟨⟩⟩
right := pair i i'
hom := (le_inf a.le b.le).hom }, _], ?_, rfl⟩
exact
List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := left i i' }⟩)
(List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := right i i' }⟩)
(List.IsChain.singleton _))
· refine
⟨[{ left := ⟨⟨⟩⟩
right := pair i' i
hom := (le_inf (b.le.trans inf_le_left) a.le).hom },
{ left := ⟨⟨⟩⟩
right := single i'
hom := (b.le.trans inf_le_left).hom }, _], ?_, rfl⟩
exact
List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := right i' i }⟩)
(List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := left i' i }⟩)
(List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := left i' j' }⟩)
(List.IsChain.singleton _)))
· refine
⟨[{ left := ⟨⟨⟩⟩
right := single i
hom := (a.le.trans inf_le_left).hom },
{ left := ⟨⟨⟩⟩
right := pair i i'
hom := (le_inf (a.le.trans inf_le_left) b.le).hom }, _], ?_, rfl⟩
exact
List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := left i j }⟩)
(List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := left i i' }⟩)
(List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := right i i' }⟩)
(List.IsChain.singleton _)))
· refine
⟨[{ left := ⟨⟨⟩⟩
right := single i
hom := (a.le.trans inf_le_left).hom },
{ left := ⟨⟨⟩⟩
right := pair i i'
hom := (le_inf (a.le.trans inf_le_left) (b.le.trans inf_le_left)).hom },
{ left := ⟨⟨⟩⟩
right := single i'
hom := (b.le.trans inf_le_left).hom }, _], ?_, rfl⟩
exact
List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := left i j }⟩)
(List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := left i i' }⟩)
(List.IsChain.cons_cons
(Or.inl
⟨{ left := 𝟙 _
right := right i i' }⟩)
(List.IsChain.cons_cons
(Or.inr
⟨{ left := 𝟙 _
right := left i' j' }⟩)
(List.IsChain.singleton _))))⟩
