exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType

English

A symmetric variant of the previous LocallyOfFiniteType result, guaranteeing the same refinement existence in the symmetric setting.

Русский

Симметричная замена предыдущего результата о LocallyOfFiniteType, гарантирующая существование refine в симметричном контексте.

LaTeX

$$$\\exists k\\ (\\mathrm{hik}: k \\to i)(\\mathrm{hjk}: k \\to j),\\ D.map\\ \\mathrm{hik} \\gg a = D.map\\ \\mathrm{hjk} \\gg b.$$$

Lean4

/-- Given a cofiltered diagram `D` of quasi-compact `S`-schemes with affine transition maps,
and another scheme `X` of finite type over `S`.
Then the canonical map `colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X)` is injective.

In other words, for each pair of `a : Homₛ(Dᵢ, X)` and `b : Homₛ(Dⱼ, X)` that give rise to the
same map `Homₛ(lim Dᵢ, X)`, there exists a `k` with `fᵢ : k ⟶ i` and `fⱼ : k ⟶ j` such that
`D(fᵢ) ≫ a = D(fⱼ) ≫ b`.
-/
@[stacks 01ZC "Injective part of (1) => (3)"]
theorem exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType {i : I} (a : D.obj i ⟶ X) (ha : t.app i = a ≫ f) {j : I}
    (b : D.obj j ⟶ X) (hb : t.app j = b ≫ f) (hab : c.π.app i ≫ a = c.π.app j ≫ b) :
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), D.map hik ≫ a = D.map hjk ≫ b := by
  classical
  wlog h : i = j
  · let o := IsCofiltered.min i j
    have :=
      this D t f c hc (D.map (IsCofiltered.minToLeft i j) ≫ a) (by simp [← ha])
        (D.map (IsCofiltered.minToRight i j) ≫ b) (by simp [← hb]) (by simpa) rfl
    obtain ⟨k, hik, hjk, heq⟩ := this
    use k, hik ≫ IsCofiltered.minToLeft i j, hjk ≫ IsCofiltered.minToRight i j
    simpa using heq
  subst h
  let A : ExistsHomHomCompEqCompAux D t f :=
    { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab
      𝒰S := S.affineCover, 𝒰X i := Scheme.affineCover _ }
  let 𝒰 := Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X
  let W := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
  choose k hki' heq using A.exists_eq
  let 𝒰Df := A.𝒰D.finiteSubcover
  rcases isEmpty_or_nonempty (D.obj A.i') with h | h
  · exact ⟨A.i', A.hii', A.hii', isInitialOfIsEmpty.hom_ext _ _⟩
  let O : Finset I := { A.i' } ∪ Finset.univ.image (fun i : 𝒰Df.I₀ ↦ k <| A.𝒰D.idx i.1)
  let o := Nonempty.some (inferInstanceAs <| Nonempty 𝒰Df.I₀)
  have ho : k (A.𝒰D.idx o.1) ∈ O := by simp [O]
  obtain ⟨l, hl1, hl2⟩ :=
    IsCofiltered.inf_exists O
      (Finset.univ.image (fun i : 𝒰Df.I₀ ↦ ⟨k <| A.𝒰D.idx i.1, A.i', by simp [O], by simp [O], hki' <| A.𝒰D.idx i.1⟩))
  have (w v : 𝒰Df.I₀) : hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx w.1) = hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx v.1) :=
    by
    trans hl1 (show A.i' ∈ O by simp [O])
    · exact hl2 _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))
    · exact .symm <| hl2 _ _ (Finset.mem_image_of_mem _ (by simp))
  refine ⟨l, hl1 ho ≫ hki' _ ≫ A.hii', hl1 ho ≫ hki' _ ≫ A.hii', ?_⟩
  apply Cover.hom_ext (𝒰Df.pullback₁ (D.map <| hl1 ho ≫ hki' _))
  intro u
  let F :
    pullback (D.map (hl1 ho ≫ hki' (A.𝒰D.idx o.1))) (𝒰Df.f u) ⟶
      pullback (D.map (hki' <| A.𝒰D.idx u.1)) (A.𝒰D.f <| A.𝒰D.idx u.1) :=
    pullback.map _ _ _ _ (D.map <| hl1 (by simp [O])) (𝟙 _) (𝟙 _) (by rw [Category.comp_id, ← D.map_comp, this]) rfl
  have hF : F ≫ pullback.fst (D.map (hki' _)) (A.𝒰D.f _) = pullback.fst _ _ ≫ D.map (hl1 (by simp [O])) := by simp [F]
  simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, PreZeroHypercover.pullback₁_X,
    PreZeroHypercover.pullback₁_f, Functor.map_comp, Category.assoc] at heq ⊢
  simp_rw [← D.map_comp_assoc, reassoc_of% this o u, D.map_comp_assoc]
  rw [← reassoc_of% hF, ← reassoc_of% hF, heq]

Похожие утверждения