English
The base map of fromGlued is injective.
Русский
Базисное отображение fromGlued инъективно.
LaTeX
$$$$ (\text{fromGlued})_{\text{base}} \text{ is injective}. $$$$
Lean4
theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.base :=
by
intro x y h
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h
simp_rw [← Scheme.comp_base] at h
rw [ι_fromGlued, ι_fromGlued] at h
let e :=
(TopCat.pullbackConeIsLimit _ _).conePointUniqueUpToIso
(isLimitOfHasPullbackOfPreservesLimit Scheme.forgetToTop (𝒰.f i) (𝒰.f j))
rw [𝒰.gluedCover.ι_eq_iff]
use e.hom ⟨⟨x, y⟩, h⟩
constructor
· erw [← ConcreteCategory.comp_apply e.hom, IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left]
rfl
· erw [← ConcreteCategory.comp_apply e.hom, pullbackSymmetry_hom_comp_fst,
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right]
rfl
