nonempty_isColimit_binaryCofanMk_of_isCompl

English

If X and Y are open disjoint covering subobjects of S, then the binary cofan Mk is a colimit.

Русский

Если X и Y — открытые непересекающиеся подсхемы, покрывающие S, то бинарный кофан Mk является колимитом.

LaTeX

$$$Nonempty\\ (IsColimit\\ (BinaryCofan.mk f g))$ under IsOpenImmersion and IsCompl conditions$$

Lean4

/-- If `X` and `Y` are open disjoint and covering open subschemes of `S`,
`S` is the disjoint union of `X` and `Y`. -/
theorem nonempty_isColimit_binaryCofanMk_of_isCompl {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) [IsOpenImmersion f]
    [IsOpenImmersion g] (hf : IsCompl f.opensRange g.opensRange) : Nonempty (IsColimit <| BinaryCofan.mk f g) :=
  by
  let c' : Cofan fun j ↦ (WalkingPair.casesOn j X Y : Scheme.{u}) := .mk S fun j ↦ WalkingPair.casesOn j f g
  let i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl _) (by rintro (b | b) <;> rfl)
  refine ⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩
  let fi (j : WalkingPair) : WalkingPair.casesOn j X Y ⟶ S := WalkingPair.casesOn j f g
  convert nonempty_isColimit_cofanMk_of fi _ _
  · intro i
    cases i <;> (simp [fi]; infer_instance)
  · simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2
  · intro i j hij
    match i, j with
    | .left, .right => simpa [fi] using hf.1
    | .right, .left => simpa [fi] using hf.1.symm

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