English
Let F1, F2, F3 be presheaves and f1: F1 → F2, f2: F2 → F3 with f3: F1 → F3 and f1 ≫ f2 = f3. If f3 is locally surjective and f2 is locally injective, then f1 is locally surjective.
Русский
Пусть F1, F2, F3 — прешафы и f1: F1 → F2, f2: F2 → F3, с f3: F1 → F3 и f1 ≫ f2 = f3. Если f3 локально сюръективен, а f2 локально инъективен, то f1 локально сюръективен.
LaTeX
$$Eq (f1 ≫ f2) f3 → IsLocallySurjective_J(f3) → IsLocallyInjective_J(f2) → IsLocallySurjective_J(f1)$$
Lean4
theorem isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂)
(f₂ : F₂ ⟶ F₃) [IsLocallySurjective J (f₁ ≫ f₂)] [IsLocallyInjective J f₂] : IsLocallySurjective J f₁ where
imageSieve_mem {X}
x := by
let S := imageSieve (f₁ ≫ f₂) (f₂.app _ x)
let T : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (_ : S f), Sieve Y := fun Y f hf =>
equalizerSieve (f₁.app _ (localPreimage (f₁ ≫ f₂) (f₂.app _ x) f hf)) (F₂.map f.op x)
refine J.superset_covering ?_ (J.transitive (imageSieve_mem J (f₁ ≫ f₂) (f₂.app _ x)) (Sieve.bind S.1 T) ?_)
· rintro Y _ ⟨Z, a, g, hg, ha, rfl⟩
exact ⟨F₁.map a.op (localPreimage (f₁ ≫ f₂) _ _ hg), by simpa using ha⟩
· intro Y f hf
apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)
apply equalizerSieve_mem J f₂
rw [NatTrans.naturality_apply, ← app_localPreimage (f₁ ≫ f₂) _ _ hf, NatTrans.comp_app,
ConcreteCategory.comp_apply]
