pushforward_cover_iff_cover_pullback

English

Another formulation of PushforwardMem that |S.functorPushforward G| ∈ K iff |S| ∈ J using the same data.

Русский

Ещё одно формулирование PushforwardMem: |S.functorPushforward G| ∈ K эквивалентно |S| ∈ J.

LaTeX

$$$S.functorPushforward G \in K \;\iff\; S \in J$$$

Lean4

theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S : Sieve X) :
    K _ (S.functorPushforward G) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S :=
  by
  constructor
  · intro hS
    exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
  · rintro ⟨T, rfl⟩
    exact LocallyCoverDense.functorPushforward_functorPullback_mem T

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