map_le_iff — Mathlib

English

For P on C, Q on D with Q respecting iso, P.map F ≤ Q is equivalent to P ≤ Q.inverseImage F.

Русский

Для P на C и Q на D с условием, что Q сохраняет изоморфизмы, P.map F ≤ Q эквивалентно P ≤ Q.inverseImage F.

LaTeX

$$$P.map F \\le Q \\iff P \\le Q^{-1}F$$$

Lean4

theorem map_le_iff (P : MorphismProperty C) {F : C ⥤ D} (Q : MorphismProperty D) [RespectsIso Q] :
    P.map F ≤ Q ↔ P ≤ Q.inverseImage F := by
  constructor
  · intro h X Y f hf
    exact h (F.map f) (map_mem_map P F f hf)
  · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact (Q.arrow_mk_iso_iff e).1 (h _ hf')

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