Geb.Mathlib.CategoryTheory.FinSetSkel.Classifier.Instance

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.Classifier.Core
public import Geb.Mathlib.CategoryTheory.FinSetSkel.Mono
public import Geb.Mathlib.CategoryTheory.FinSetSkel.Shapes.Instances
public import Mathlib.CategoryTheory.Subobject.Classifier.Defs

The subobject classifier of `FinSetSkel`

The mathlib packaging of FinSetSkel.Classifier.chi and its universal property. The classifying object is the object of length 2, Ω₀ is the one-element terminal object, and truth picks the index 1; the characteristic morphism sends the members of a monomorphism's image to 1. This module and the module defining FinSetSkel.Classifier.chi fix that orientation jointly, each stating it.

Main definitions

FinSetSkel.truth — the truth morphism.

FinSetSkel.classifier — the subobject classifier.

Main statements

FinSetSkel.chi_iff_of_isPullback — the fibre of a classifying morphism over 1 is the image of the monomorphism it classifies.

Implementation notes

The derivation of the vector-level hypothesis of FinSetSkel.Classifier.chi_uniq from IsPullback lives here rather than in the choice-free layer, and it is content rather than packaging: it uses the pullback's universal property and cannot be stated choice-free.

Ω₀ is the object mk 1, which the cartesian structure also takes as its unit, so the classifier's Ω₀ and the cartesian unit are the same object and their comparison is an isomorphism between an object and itself.

References

[Freyd1972], for the axiomatisation whose subobject classifier FinSetSkel.classifier supplies.

Tags

finite sets, skeleton, subobject classifier, topos

              @[expose] public sectionuniverse uopen CategoryTheory Limitsnamespace FinSetSkel

The truth morphism: the point of the classifying object at index 1.

def truth : (mk 1 : FinSetSkel.{u}) ⟶ mk 2 := point 1

The fibre of a classifying morphism over 1 is the image of the monomorphism it classifies.

theorem chi_iff_of_isPullback {U X : FinSetSkel.{u}} (m : U ⟶ X)
    (χ' : X ⟶ mk 2)
    (hp : IsPullback m (isTerminalOne.from U) χ' truth) (j : Fin X.len) :
    χ'.toVec.get j = 1 ↔ j ∈ m.toVec.toList := byU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.len⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
  -- (←) the square commutes, and both of its legs are the constant `1`
  have hmpr : j ∈ m.toVec.toList → χ'.toVec.get j = 1 := by
    intro hjU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toList⊢ (Hom.toVec χ').get j = 1
    obtain ⟨n, hn, hget⟩ := List.mem_iff_getElem.mp hjU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = j⊢ (Hom.toVec χ').get j = 1
    have hi : n < U.len := byU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.len⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList simpa using hnU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.len⊢ (Hom.toVec χ').get j = 1
    have hj' : m.toVec.get ⟨n, hi⟩ = j := byU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.len⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
      rw [Vector.get_eq_getElemU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.len⊢ (Hom.toVec m)[↑⟨n, hi⟩] = j]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.len⊢ (Hom.toVec m)[↑⟨n, hi⟩] = j
      simpa using hgetU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = j⊢ (Hom.toVec χ').get j = 1
    have hw : (m ≫ χ').toVec.get ⟨n, hi⟩
        = (isTerminalOne.from U ≫ truth).toVec.get ⟨n, hi⟩ :=
      congrArg (fun k : U ⟶ mk 2 ↦ k.toVec.get ⟨n, hi⟩) hp.wU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec (m ≫ χ')).get ⟨n, hi⟩ = (Hom.toVec (isTerminalOne.from U ≫ truth)).get ⟨n, hi⟩⊢ (Hom.toVec χ').get j = 1
    rw [comp_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = (Hom.toVec (isTerminalOne.from U ≫ truth)).get ⟨n, hi⟩⊢ (Hom.toVec χ').get j = 1 comp_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = (Hom.toVec truth).get ((Hom.toVec (isTerminalOne.from U)).get ⟨n, hi⟩)⊢ (Hom.toVec χ').get j = 1 truth,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) =
  (Hom.toVec (point 1)).get ((Hom.toVec (isTerminalOne.from U)).get ⟨n, hi⟩)⊢ (Hom.toVec χ').get j = 1 point_getU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1⊢ (Hom.toVec χ').get j = 1] at hwU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1⊢ (Hom.toVec χ').get j = 1
    rw [← hj'U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1⊢ (Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhj:j ∈ (Hom.toVec m).toListn:ℕhn:n < (Hom.toVec m).toList.lengthhget:(Hom.toVec m).toList[n] = jhi:n < U.lenhj':(Hom.toVec m).get ⟨n, hi⟩ = jhw:(Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1⊢ (Hom.toVec χ').get ((Hom.toVec m).get ⟨n, hi⟩) = 1
    exact hwU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
  -- (→) the point at `j` factors through the pullback
  have hmp : χ'.toVec.get j = 1 → j ∈ m.toVec.toList := by
    intro hU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1⊢ j ∈ (Hom.toVec m).toList
    have hw : point j ≫ χ' = isTerminalOne.from (mk 1) ≫ truth := byU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.len⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
      refine hom_ext fun _ ↦ ?_U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec (point j ≫ χ')).get x✝ = (Hom.toVec (isTerminalOne.from { len := 1 } ≫ truth)).get x✝
      rw [comp_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get ((Hom.toVec (point j)).get x✝) = (Hom.toVec (isTerminalOne.from { len := 1 } ≫ truth)).get x✝ comp_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get ((Hom.toVec (point j)).get x✝) =
  (Hom.toVec truth).get ((Hom.toVec (isTerminalOne.from { len := 1 })).get x✝) point_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get j = (Hom.toVec truth).get ((Hom.toVec (isTerminalOne.from { len := 1 })).get x✝) truth,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get j = (Hom.toVec (point 1)).get ((Hom.toVec (isTerminalOne.from { len := 1 })).get x✝) point_getU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get j = 1]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1x✝:Fin { len := 1 }.len⊢ (Hom.toVec χ').get j = 1
      exact hU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truth⊢ j ∈ (Hom.toVec m).toList
    obtain ⟨l, hl⟩ : ∃ l : (mk 1 : FinSetSkel.{u}) ⟶ U, l ≫ m = point j :=
      ⟨hp.lift (point j) (isTerminalOne.from (mk 1)) hw,
        hp.lift_fst (point j) (isTerminalOne.from (mk 1)) hw⟩U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point j⊢ j ∈ (Hom.toVec m).toList
    have hg : m.toVec.get (l.toVec.get 0) = j := byU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.len⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
      rw [← comp_get,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point j⊢ (Hom.toVec (l ≫ m)).get 0 = j hl,U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point j⊢ (Hom.toVec (point j)).get 0 = j point_getU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point j⊢ j = j]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point jhg:(Hom.toVec m).get ((Hom.toVec l).get 0) = j⊢ j ∈ (Hom.toVec m).toList
    rw [← hgU:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point jhg:(Hom.toVec m).get ((Hom.toVec l).get 0) = j⊢ (Hom.toVec m).get ((Hom.toVec l).get 0) ∈ (Hom.toVec m).toList]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1h:(Hom.toVec χ').get j = 1hw:point j ≫ χ' = isTerminalOne.from { len := 1 } ≫ truthl:{ len := 1 } ⟶ Uhl:l ≫ m = point jhg:(Hom.toVec m).get ((Hom.toVec l).get 0) = j⊢ (Hom.toVec m).get ((Hom.toVec l).get 0) ∈ (Hom.toVec m).toList
    simp [Vector.get_eq_getElem]U:FinSetSkelX:FinSetSkelm:U ⟶ Xχ':X ⟶ { len := 2 }hp:IsPullback m (isTerminalOne.from U) χ' truthj:Fin X.lenhmpr:j ∈ (Hom.toVec m).toList → (Hom.toVec χ').get j = 1hmp:(Hom.toVec χ').get j = 1 → j ∈ (Hom.toVec m).toList⊢ (Hom.toVec χ').get j = 1 ↔ j ∈ (Hom.toVec m).toList
  exact ⟨hmp, hmpr⟩All goals completed! 🐙

The subobject classifier of FinSetSkel.

def classifier : Subobject.Classifier FinSetSkel.{u} :=
  Subobject.Classifier.mkOfTerminalΩ₀ (mk 1) isTerminalOne (mk 2) truth
    (fun m ↦ Classifier.chi m)
    (fun m _ ↦ byU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono m⊢ IsPullback m (isTerminalOne.from U✝) (Classifier.chi m) truth
      have hinj : Function.Injective m.toVec.get := mono_iff_injective.mp ‹Mono m›U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).get⊢ IsPullback m (isTerminalOne.from U✝) (Classifier.chi m) truth
      -- the square: both legs are the constant `1` on the image of `m`
      have hsq : CommSq m (isTerminalOne.from _) (Classifier.chi m) truth :=
        ⟨hom_ext fun i ↦ byU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (m ≫ Classifier.chi m)).get i = (Hom.toVec (isTerminalOne.from U✝ ≫ truth)).get i
          rw [comp_get,U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (Classifier.chi m)).get ((Hom.toVec m).get i) = (Hom.toVec (isTerminalOne.from U✝ ≫ truth)).get i comp_get,U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (Classifier.chi m)).get ((Hom.toVec m).get i) =
  (Hom.toVec truth).get ((Hom.toVec (isTerminalOne.from U✝)).get i) truth,U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (Classifier.chi m)).get ((Hom.toVec m).get i) =
  (Hom.toVec (point 1)).get ((Hom.toVec (isTerminalOne.from U✝)).get i) point_getU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (Classifier.chi m)).get ((Hom.toVec m).get i) = 1]U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).geti:Fin U✝.len⊢ (Hom.toVec (Classifier.chi m)).get ((Hom.toVec m).get i) = 1
          exact Classifier.chi_get_image_eq_one m iAll goals completed! 🐙⟩U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truth⊢ IsPullback m (isTerminalOne.from U✝) (Classifier.chi m) truth
      -- membership of a competing cone's left leg, from its own commutation
      have hmem : ∀ (s : PullbackCone (Classifier.chi m) truth) (t : Fin s.pt.len),
          s.fst.toVec.get t ∈ m.toVec.toList := fun s t ↦
        (Classifier.chiVec_get_eq_one_iff m _).mp (byU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.len⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1
          have hc : (s.fst ≫ Classifier.chi m).toVec.get t
              = (s.snd ≫ truth).toVec.get t :=
            congrArg (fun k : s.pt ⟶ mk 2 ↦ k.toVec.get t) s.conditionU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.lenhc:(Hom.toVec (s.fst ≫ Classifier.chi m)).get t = (Hom.toVec (s.snd ≫ truth)).get t⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1
          rw [comp_get,U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.lenhc:(Hom.toVec (Classifier.chi m)).get ((Hom.toVec s.fst).get t) = (Hom.toVec (s.snd ≫ truth)).get t⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1 comp_get,U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.lenhc:(Hom.toVec (Classifier.chi m)).get ((Hom.toVec s.fst).get t) = (Hom.toVec truth).get ((Hom.toVec s.snd).get t)⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1 Classifier.chi_getU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.lenhc:(Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = (Hom.toVec truth).get ((Hom.toVec s.snd).get t)⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1] at hcU✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truths:PullbackCone (Classifier.chi m) trutht:Fin s.pt.lenhc:(Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = (Hom.toVec truth).get ((Hom.toVec s.snd).get t)⊢ (Classifier.chiVec m).get ((Hom.toVec s.fst).get t) = 1
          exact hc.trans (point_get 1 _)All goals completed! 🐙)U✝:FinSetSkelX✝:FinSetSkelm:U✝ ⟶ X✝x✝:Mono mhinj:Function.Injective (Hom.toVec m).gethsq:CommSq m (isTerminalOne.from U✝) (Classifier.chi m) truthhmem:∀ (s : PullbackCone (Classifier.chi m) truth) (t : Fin s.pt.len), (Hom.toVec s.fst).get t ∈ (Hom.toVec m).toList⊢ IsPullback m (isTerminalOne.from U✝) (Classifier.chi m) truth
      exact IsPullback.of_isLimit' hsq
        (PullbackCone.isLimitAux _
          (fun s ↦ Classifier.pullbackLift m hinj s.fst (hmem s))
          (fun s ↦ Classifier.pullbackLift_comp m hinj s.fst (hmem s))
          (fun _ ↦ (toOne_uniq _).trans (toOne_uniq _).symm)
          (fun s n hn ↦
            Classifier.pullbackLift_uniq m hinj s.fst (hmem s) n
              (hn WalkingCospan.left)))All goals completed! 🐙)
    (fun m _ χ' hp ↦ Classifier.chi_uniq m χ' (chi_iff_of_isPullback m χ' hp))

end FinSetSkel

The subobject classifier of FinSetSkel