Geb.Mathlib.CategoryTheory.FinSetSkel.Mono

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Mathlib.CategoryTheory.FinSetSkel.Shapes.Core

Monomorphisms of `FinSetSkel`

A morphism is a monomorphism exactly when its vector is injective.

Main statements

FinSetSkel.mono_iff_injective — monomorphisms are the morphisms with injective vectors.

Implementation notes

CategoryTheory.Mono and CategoryTheory.Category are both axiom-free, so the statement belongs in the choice-free layer, and the proof is direct over vectors: the forward direction tests a morphism against two points, and the reverse is FinSetSkel.hom_ext.

It supplies the hypothesis Vector.invOfInjective takes, and so is a prerequisite of the subobject classifier rather than a free-standing characterisation.

Tags

finite sets, skeleton, monomorphism, injective

              @[expose] public sectionuniverse uopen CategoryTheorynamespace FinSetSkel

A morphism is a monomorphism exactly when its vector is injective.

theorem mono_iff_injective {X Y : FinSetSkel.{u}} {f : X ⟶ Y} :
    Mono f ↔ Function.Injective f.toVec.get := byX:FinSetSkelY:FinSetSkelf:X ⟶ Y⊢ Mono f ↔ Function.Injective (Hom.toVec f).get
  constructormpX:FinSetSkelY:FinSetSkelf:X ⟶ Y⊢ Mono f → Function.Injective (Hom.toVec f).getmprX:FinSetSkelY:FinSetSkelf:X ⟶ Y⊢ Function.Injective (Hom.toVec f).get → Mono f
  ·mpX:FinSetSkelY:FinSetSkelf:X ⟶ Y⊢ Mono f → Function.Injective (Hom.toVec f).get intro hm i j hijmpX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get j⊢ i = j
    have h : point i ≫ f = point j ≫ f :=
      hom_ext fun t ↦ byX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec (point i ≫ f)).get t = (Hom.toVec (point j ≫ f)).get t rw [comp_get,X:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec f).get ((Hom.toVec (point i)).get t) = (Hom.toVec (point j ≫ f)).get t comp_get,X:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec f).get ((Hom.toVec (point i)).get t) = (Hom.toVec f).get ((Hom.toVec (point j)).get t) point_get,X:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec f).get i = (Hom.toVec f).get ((Hom.toVec (point j)).get t) point_get,X:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec f).get i = (Hom.toVec f).get j hijX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jt:Fin { len := 1 }.len⊢ (Hom.toVec f).get j = (Hom.toVec f).get j]mpX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jh:point i ≫ f = point j ≫ f⊢ i = j
    have hp : (point i : mk 1 ⟶ X) = point j := (cancel_mono f).mp hmpX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jh:point i ≫ f = point j ≫ fhp:point i = point j⊢ i = j
    have := congrArg (fun m ↦ (m : mk 1 ⟶ X).toVec.get 0) hpmpX:FinSetSkelY:FinSetSkelf:X ⟶ Yhm:Mono fi:Fin X.lenj:Fin X.lenhij:(Hom.toVec f).get i = (Hom.toVec f).get jh:point i ≫ f = point j ≫ fhp:point i = point jthis:(Hom.toVec (point i)).get 0 = (Hom.toVec (point j)).get 0⊢ i = j
    simpa only [point_get] using thisAll goals completed! 🐙
  ·mprX:FinSetSkelY:FinSetSkelf:X ⟶ Y⊢ Function.Injective (Hom.toVec f).get → Mono f intro hinjmprX:FinSetSkelY:FinSetSkelf:X ⟶ Yhinj:Function.Injective (Hom.toVec f).get⊢ Mono f
    constructormprX:FinSetSkelY:FinSetSkelf:X ⟶ Yhinj:Function.Injective (Hom.toVec f).get⊢ ∀ {Z : FinSetSkel} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
    intro Z g h hghmprX:FinSetSkelY:FinSetSkelf:X ⟶ Yhinj:Function.Injective (Hom.toVec f).getZ:FinSetSkelg:Z ⟶ Xh:Z ⟶ Xhgh:g ≫ f = h ≫ f⊢ g = h
    exact hom_ext fun t ↦ hinj (byX:FinSetSkelY:FinSetSkelf:X ⟶ Yhinj:Function.Injective (Hom.toVec f).getZ:FinSetSkelg:Z ⟶ Xh:Z ⟶ Xhgh:g ≫ f = h ≫ ft:Fin Z.len⊢ (Hom.toVec f).get ((Hom.toVec g).get t) = (Hom.toVec f).get ((Hom.toVec h).get t)
      have := congrArg (fun m ↦ (m : Z ⟶ Y).toVec.get t) hghX:FinSetSkelY:FinSetSkelf:X ⟶ Yhinj:Function.Injective (Hom.toVec f).getZ:FinSetSkelg:Z ⟶ Xh:Z ⟶ Xhgh:g ≫ f = h ≫ ft:Fin Z.lenthis:(Hom.toVec (g ≫ f)).get t = (Hom.toVec (h ≫ f)).get t⊢ (Hom.toVec f).get ((Hom.toVec g).get t) = (Hom.toVec f).get ((Hom.toVec h).get t)
      simpa only [comp_get] using thisAll goals completed! 🐙)

end FinSetSkel

Monomorphisms of FinSetSkel

Main statements

Implementation notes

Tags

Monomorphisms of `FinSetSkel`