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