eval_section_injective_of_eventually_injective

English

If F.map f is injective for every morphism f, then evaluation at a fixed j, considered as a function from sections to the fiber F.obj j, is injective.

Русский

Если отображение F.map f инъективно для каждого морфизма f, то отображение s ↦ s.val j на секциях F.sections инъективно.

LaTeX

$$$\forall i,\forall f : i \to j,\ (F.map f)\text{Injective} \Rightarrow (\lambda s : F.sections. -> s.val j)\text{Injective}.$$$

Lean4

theorem eval_section_injective_of_eventually_injective {j} (Finj : ∀ (i) (f : i ⟶ j), (F.map f).Injective) (i)
    (f : i ⟶ j) : (fun s : F.sections => s.val j).Injective :=
  by
  refine fun s₀ s₁ h => Subtype.ext <| funext fun k => ?_
  obtain ⟨m, mi, mk, _⟩ := IsCofilteredOrEmpty.cone_objs i k
  dsimp at h
  rw [← s₀.prop (mi ≫ f), ← s₁.prop (mi ≫ f)] at h
  rw [← s₀.prop mk, ← s₁.prop mk]
  exact congr_arg _ (Finj m (mi ≫ f) h)

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