instEssSurjNonemptyFinLinOrdSkeletalFunctor

English

The skeletal functor is essentially surjective on objects of NonemptyFinLinOrd, i.e., every object is isomorphic to an image of a skeletal object.

Русский

Скелетный функтор является существенно сюръективным на объектах NonemptyFinLinOrd: каждый объект изоморфен образу скелетного объекта.

LaTeX

$$$\\text{EssSurj}_{\text{skeletalFunctor}}$$$

Lean4

instance : skeletalFunctor.EssSurj where
  mem_essImage
    X :=
    ⟨⦋(Fintype.card X - 1 : ℕ)⦌,
      ⟨by
        have aux : Fintype.card X = Fintype.card X - 1 + 1 :=
          (Nat.succ_pred_eq_of_pos <| Fintype.card_pos_iff.mpr ⟨⊥⟩).symm
        let f := monoEquivOfFin X aux
        have hf := (Finset.univ.orderEmbOfFin aux).strictMono
        refine
          { hom := LinOrd.ofHom ⟨f, hf.monotone⟩
            inv := LinOrd.ofHom ⟨f.symm, ?_⟩
            hom_inv_id := by ext; apply f.symm_apply_apply
            inv_hom_id := by ext; apply f.apply_symm_apply }
        intro i j h
        change f.symm i ≤ f.symm j
        rw [← hf.le_iff_le]
        change f (f.symm i) ≤ f (f.symm j)
        simpa only [OrderIso.apply_symm_apply]⟩⟩

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