English
If S is an object of the base category and E is a pre-1-hypercover of S which admits pullbacks, together with a covering of S and a family of coverings for all pullback fibers, then mk' produces a genuine 1-hypercover of S.
Русский
Если S — объект базовой категории, и E является пред-1-гиперпокрытием S, допускающим вытяжки, при этом дано покрытие S и для каждой пары индексов существуют покрытия соответствующих фибер-перемножителей, то конструктор mk' задаёт настоящее 1-гор Cover(S).
LaTeX
$$$mk' : \forall {S} (E : \mathrm{PreOneHypercover} S) [E.HasPullbacks] (mem_0 : E.sieve_0 \in J S) (mem_1' : \forall i_1 i_2, E.sieve_1' i_1 i_2 \in J _), J.OneHypercover S$$$
Lean4
/-- In order to check that a certain data is a `1`-hypercover of `S`, it suffices to
check that the data provides a covering of `S` and of the fibre products. -/
@[simps toPreOneHypercover]
def mk' {S : C} (E : PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S)
(mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J _) : J.OneHypercover S
where
toPreOneHypercover := E
mem₀ := mem₀
mem₁ i₁ i₂ W p₁ p₂
w := by
rw [E.sieve₁_eq_pullback_sieve₁' _ _ w]
exact J.pullback_stable' _ (mem₁' i₁ i₂)
