mk_map_eq_iff_of_mono — Mathlib

English

If f is mono, then S.mk(X.map f.op x) = S.mk x if and only if f is an isomorphism.

Русский

Если f моно, то S.mk(X.map f.op x) = S.mk x тогда и только тогда, когда f является изоморфизмом.

LaTeX

$$$\text{S.mk}(X.map\ f.op\ x) = \text{S.mk}(x) \iff \text{IsIso}(f)$$$

Lean4

theorem mk_map_eq_iff_of_mono {n m : ℕ} (x : X _⦋n⦌) (f : ⦋m⦌ ⟶ ⦋n⦌) [Mono f] :
    S.mk (X.map f.op x) = S.mk x ↔ IsIso f := by
  constructor
  · intro h
    obtain rfl := S.dim_eq_of_mk_eq h
    obtain rfl := SimplexCategory.eq_id_of_mono f
    infer_instance
  · intro hf
    obtain rfl := SimplexCategory.eq_of_isIso f
    obtain rfl := SimplexCategory.eq_id_of_isIso f
    simp

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