sheafify_le — Mathlib

English

If G ≤ G' and both are J-sheaves, then G.sheafify J ≤ G'.

Русский

Если G ≤ G' и обе являются шарфами J, то G.sheafify J ≤ G'.

LaTeX

$$$ G \\le G' \\;\\to\\; IsSheaf(J, G'.toPresheaf) \\Rightarrow G.sheafify J \\le G' $$$

Lean4

theorem sheafify_le (h : G ≤ G') (hF : Presieve.IsSheaf J F) (hG' : Presieve.IsSheaf J G'.toPresheaf) :
    G.sheafify J ≤ G' := by
  intro U x hx
  convert ((G.sheafifyLift (Subpresheaf.homOfLe h) hG').app U ⟨x, hx⟩).2
  apply (hF _ hx).isSeparatedFor.ext
  intro V i hi
  have :=
    congr_arg (fun f : G.toPresheaf ⟶ G'.toPresheaf => (NatTrans.app f (op V) ⟨_, hi⟩).1)
      (G.to_sheafifyLift (Subpresheaf.homOfLe h) hG')
  convert this.symm
  rw [← Subpresheaf.nat_trans_naturality]
  rfl

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