English
If the base map f: X → Y has an injective underlying map, then the diagonal range of the pullback cover is the whole space: diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤.
Русский
Если базовое отображение f: X → Y инъективно на уровне пространств, то диагональный диапазон покрытия вытяжки равен всей площадке: diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤.
LaTeX
$$$\operatorname{diagonalCoverDiagonalRange}(f, \mathcal{U}, \mathcal{V}) = \top$$$
Lean4
theorem diagonalCoverDiagonalRange_eq_top_of_injective (hf : Function.Injective f.base) :
diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤ := by
rw [← top_le_iff]
rintro x -
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]
have H : (pullback.fst f f).base x = (pullback.snd f f).base x :=
hf (by rw [← Scheme.comp_base_apply, ← Scheme.comp_base_apply, pullback.condition])
let i := 𝒰.idx (f.base ((pullback.fst f f).base x))
obtain ⟨y : 𝒰.X i, hy : (𝒰.f i).base y = f.base _⟩ := 𝒰.covers (f.base ((pullback.fst f 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, ?_⟩
simp_rw [diagonalCover_map]
change x ∈ Set.range _
simp only [diagonalCover, openCoverOfBase_I₀, Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
PreZeroHypercover.pullback₁_X, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, openCoverOfBase_X,
PreZeroHypercover.bind_X, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X]
rw [range_map]
simp [← H, ← hz₁, ← hy]
