compatiblePreservingOfDownwardsClosed

English

If the given downwards-closed condition holds, then CompatiblePreserving K G is satisfied.

Русский

Если соблюдается условие нисходящей замкнутости, то выполняется CompatiblePreserving.

LaTeX

$$$\text{CompatiblePreserving } K G$$$

Lean4

theorem compatiblePreservingOfDownwardsClosed (F : C ⥤ D) [F.Full] [F.Faithful]
    (hF : ∀ {c : C} {d : D} (_ : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : CompatiblePreserving K F :=
  by
  constructor
  introv hx he
  obtain ⟨X', e⟩ := hF f₁
  apply (ℱ.1.mapIso e.op).toEquiv.injective
  simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← FunctorToTypes.map_comp_apply]
  simpa using hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂ (F.map_injective <| by simpa using he)

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