ext — Mathlib

Lean4
/-- Extensionality via Coyoneda. The typical usage would be
```
-- Goal is `X ≅ Y`
apply Coyoneda.ext
-- Goals are now functions `(X ⟶ Z) → (Y ⟶ Z)`, `(Y ⟶ Z) → (X ⟶ Z)`, and the fact that these
-- functions are inverses and natural in `Z`.
```
-/
def ext (X Y : C) (p : ∀ {Z : C}, (X ⟶ Z) → (Y ⟶ Z)) (q : ∀ {Z : C}, (Y ⟶ Z) → (X ⟶ Z))
    (h₁ : ∀ {Z : C} (f : X ⟶ Z), q (p f) = f) (h₂ : ∀ {Z : C} (f : Y ⟶ Z), p (q f) = f)
    (n : ∀ {Z Z' : C} (f : Y ⟶ Z) (g : Z ⟶ Z'), q (f ≫ g) = q f ≫ g) : X ≅ Y :=
  fullyFaithful.preimageIso
      (NatIso.ofComponents
        (fun Z =>
          { hom := q
            inv := p })) |>.unop
Похожие утверждения