English
If the composite f1 ≫ f2 is locally surjective, then f2 is locally surjective.
Русский
Если композиция f1 ≫ f2 локально сюрьективна, тогда и f2 локально сюрьективен.
LaTeX
$$$\text{IsLocallySurjective}_J(f_1 \circ f_2) \Rightarrow \text{IsLocallySurjective}_J(f_2)$$$
Lean4
instance isLocallySurjective_comp {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [IsLocallySurjective J f₁]
[IsLocallySurjective J f₂] : IsLocallySurjective J (f₁ ≫ f₂) where
imageSieve_mem
s :=
by
have : (Sieve.bind (imageSieve f₂ s) fun _ _ h => imageSieve f₁ h.choose) ≤ imageSieve (f₁ ≫ f₂) s :=
by
rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
refine ⟨t', ?_⟩
rw [op_comp, F₃.map_comp, NatTrans.comp_app, ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ht',
NatTrans.naturality_apply, H.choose_spec]
apply J.superset_covering this
apply J.bind_covering
· apply imageSieve_mem
· intros; apply imageSieve_mem
