English
The range of the diagonal of the pullback lies inside the diagonal range: range of pullback.diagonal f is contained in diagonalCoverDiagonalRange f 𝒰 𝒱.
Русский
Область диагонали вытяжки лежит внутри диагонального диапазона: множество образов pullback.diagonal f ⊆ diagonalCoverDiagonalRange f 𝒰 𝒱.
LaTeX
$$$\mathrm{range}(\mathrm{pullback.diagonal}\ f).\mathrm{base} \subseteq \operatorname{diagonalCoverDiagonalRange}(f, \mathcal{U}, \mathcal{V})$$$
Lean4
theorem range_diagonal_subset_diagonalCoverDiagonalRange :
Set.range (pullback.diagonal f).base ⊆ diagonalCoverDiagonalRange f 𝒰 𝒱 :=
by
rintro _ ⟨x, rfl⟩
simp only [diagonalCoverDiagonalRange, openCoverOfBase_I₀, openCoverOfBase_X, openCoverOfLeftRight_I₀, Opens.iSup_mk,
Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.coe_mk, Set.mem_iUnion, Set.mem_range, Sigma.exists]
let i := 𝒰.idx (f.base x)
obtain ⟨y : 𝒰.X i, hy : (𝒰.f i).base y = f.base x⟩ := 𝒰.covers (f.base x)
obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm
let j := (𝒱 i).idx z
obtain ⟨w : (𝒱 i).X j, hy : ((𝒱 i).f j).base w = z⟩ := (𝒱 i).covers z
refine ⟨i, j, (pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))).base w, ?_⟩
rw [← hz₁, ← hy, ← Scheme.comp_base_apply, ← Scheme.comp_base_apply]
simp only [diagonalCover, openCoverOfBase_I₀, Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
PreZeroHypercover.pullback₁_X, Cover.pullbackHom, Precoverage.ZeroHypercover.bind_toPreZeroHypercover,
openCoverOfBase_X, PreZeroHypercover.bind_X, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X,
PreZeroHypercover.bind_f, openCoverOfLeftRight_f, openCoverOfBase_f, comp_coeBase, TopCat.hom_comp,
ContinuousMap.comp_apply, ContinuousMap.comp_assoc]
simp_rw [← Scheme.comp_base_apply]
congr 5
apply pullback.hom_ext <;> simp
