functorPullback_pushforward_covering

English

A restatement of the equivalence using a simplified simp-lemma form for isSheaf_iff_isLimit_coverage.

Русский

Переформулирование эквивалентности через упрощенный формализм simp-леммы для isSheaf_iff_isLimit_coverage.

LaTeX

$$$\\text{IsSheaf}_{K^{\\mathrm{Gro}}}(P) \\iff \\forall X,R \\in K X, \\, \\text{Nonempty}(\\dots)$$$

Lean4

theorem functorPullback_pushforward_covering [G.IsCoverDense K] [G.IsLocallyFull K] {X : C} (T : K (G.obj X)) :
    (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X) :=
  by
  refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_
  apply K.transitive (G.is_cover_of_isCoverDense _ _) _
  rintro W _ ⟨Z, iWZ, iZY, rfl⟩
  rw [Sieve.pullback_comp]; apply K.pullback_stable; clear W iWZ
  apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))
  rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩
  exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩

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