ext_elem — Mathlib

English

Miscellaneous simp lemmas about ext_elem specialized to OpenCover.

Русский

Различные вспомогательные леммы для ext_elem, применяемые к OpenCover.

LaTeX

$$$$ \text{simp lemmas for ext_elem on OpenCover} $$$$

Lean4

/-- If two global sections agree after restriction to each member of an open cover, then
they agree globally. -/
theorem ext_elem {X : Scheme.{u}} {U : X.Opens} (f g : Γ(X, U)) (𝒰 : X.OpenCover)
    (h : ∀ i : 𝒰.I₀, (𝒰.f i).app U f = (𝒰.f i).app U g) : f = g :=
  by
  fapply
    TopCat.Sheaf.eq_of_locally_eq' X.sheaf (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
  · intro x hx
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.coe_mk, Set.mem_iUnion,
      Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
    refine ⟨?_, hx⟩
    simpa using ⟨_, 𝒰.covers x⟩
  · intro x
    replace h := h (𝒰.idx x)
    rw [← IsOpenImmersion.map_ΓIso_inv] at h
    exact (IsOpenImmersion.ΓIso (𝒰.f (𝒰.idx x)) U).commRingCatIsoToRingEquiv.symm.injective h

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