mono_of_nonDegenerate — Mathlib

English

If x is non-degenerate and x = X.map f.op y with epi f, then f is mono.

Русский

Если x недегенеративен и x = X.map f.op y с эпиморфизмом f, то f моно.

LaTeX

$$$ x \in X_{\text{nonDegenerate}}(n) \Rightarrow \big( f: [n] \to m \big) [\text{Epi } f] \Rightarrow \text{Mono}(f) $$$

Lean4

theorem mono_of_nonDegenerate (x : X.nonDegenerate n) {m : SimplexCategory} (f : ⦋n⦌ ⟶ m) (y : X.obj (op m))
    (hy : X.map f.op y = x) : Mono f :=
  by
  have :=
    X.isIso_of_nonDegenerate x (factorThruImage f) (y := X.map (image.ι f).op y)
      (by rw [← FunctorToTypes.map_comp_apply, ← op_comp, image.fac f, hy])
  rw [← image.fac f]
  infer_instance

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