comp_isLocallyInjective_iff — Mathlib

English

Let F1, F2, F3 be presheaves and f1: F1 → F2, f2: F2 → F3 with IsLocallyInjective J f1 and IsLocallySurjective J f1. Then IsLocallyInjective J (f1 ≫ f2) iff IsLocallyInjective J f2.

Русский

Пусть f1 и f2 — прешафы, и для f1 выполняются локальная инъективность и локальная сюръективность. Тогда IsLocallyInjective J (f1 ≫ f2) эквивалентно IsLocallyInjective J f2.

LaTeX

$$IsLocallyInjective_J(f1) ∧ IsLocallySurjective_J(f1) ⇒ (IsLocallyInjective_J(f1 ≫ f2) ↔ IsLocallyInjective_J(f2))$$

Lean4

theorem comp_isLocallyInjective_iff {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [IsLocallyInjective J f₁]
    [IsLocallySurjective J f₁] : IsLocallyInjective J (f₁ ≫ f₂) ↔ IsLocallyInjective J f₂ :=
  by
  constructor
  · intro
    exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂
  · intro
    infer_instance

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