degenerate_iff_of_isIso — Mathlib

English

Let f: X → Y be an isomorphism. Then for every n and x ∈ X.obj(n), x is degenerate in X if and only if f.app(n)(x) is degenerate in Y.

Русский

Пусть f: X → Y — изоморфизм. Тогда для каждого n и x ∈ X.obj(n) выполняется: x вырожден в X тогда и только тогда, когда f.app(n)(x) вырожден в Y.

LaTeX

$$$$\text{IsIso}(f) \Rightarrow \bigl( f.app_{n}(x) \in Y_{\mathrm{deg}}(n) \iff x \in X_{\mathrm{deg}}(n) \bigr),$$$$

Lean4

theorem degenerate_iff_of_isIso (f : X ⟶ Y) [IsIso f] {n : ℕ} (x : X _⦋n⦌) :
    f.app _ x ∈ Y.degenerate n ↔ x ∈ X.degenerate n :=
  by
  constructor
  · intro hy
    simpa [← FunctorToTypes.comp] using degenerate_app_apply hy (inv f)
  · exact fun hx ↦ degenerate_app_apply hx f

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