-- Initial, terminal, and zero objects
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Category.Terminal
import MonoEpi

-- A terminal object receives exactly one morphism from each object, an
-- initial object sends exactly one morphism to each object.
predicate Terminal (C t : Set) :=
  t ∈ obj(C) ∧ (∀ a ∈ obj(C), ∃ f ∈ hom(C, a, t),
    ∀ g ∈ hom(C, a, t), g = f)

predicate Initial (C i : Set) :=
  i ∈ obj(C) ∧ (∀ a ∈ obj(C), ∃ f ∈ hom(C, i, a),
    ∀ g ∈ hom(C, i, a), g = f)

predicate ZeroObject (C z : Set) :=
  Initial(C, z) ∧ Terminal(C, z)

theorem Terminal.object (C t : Set)
  requires terminal : Terminal(C, t)
  shows t ∈ obj(C)
proof
  obtain ⟨tInO, universal⟩ := terminal
  exact tInO

theorem Terminal.exists_morphism (C t a : Set)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  shows ∃ f ∈ hom(C, a, t), ∀ g ∈ hom(C, a, t), g = f
proof
  obtain ⟨tInO, universal⟩ := terminal
  exact universal with a, aInO

theorem Terminal.unique_morphism (C t a f g : Set)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  requires fHom : f ∈ hom(C, a, t)
  requires gHom : g ∈ hom(C, a, t)
  shows f = g
proof
  obtain ⟨u, uHom, unique⟩ := Terminal.exists_morphism with terminal, aInO
  have fEqual := unique with f, fHom
  have gEqual := unique with g, gHom
  cc

theorem Initial.object (C i : Set)
  requires initial : Initial(C, i)
  shows i ∈ obj(C)
proof
  obtain ⟨iInO, universal⟩ := initial
  exact iInO

theorem Initial.exists_morphism (C i a : Set)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  shows ∃ f ∈ hom(C, i, a), ∀ g ∈ hom(C, i, a), g = f
proof
  obtain ⟨iInO, universal⟩ := initial
  exact universal with a, aInO

theorem Initial.unique_morphism (C i a f g : Set)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  requires fHom : f ∈ hom(C, i, a)
  requires gHom : g ∈ hom(C, i, a)
  shows f = g
proof
  obtain ⟨u, uHom, unique⟩ := Initial.exists_morphism with initial, aInO
  have fEqual := unique with f, fHom
  have gEqual := unique with g, gHom
  cc

theorem ZeroObject.initial (C z : Set)
  requires zero : ZeroObject(C, z)
  shows Initial(C, z)
proof
  simp [ZeroObject]

theorem ZeroObject.terminal (C z : Set)
  requires zero : ZeroObject(C, z)
  shows Terminal(C, z)
proof
  simp [ZeroObject]

theorem ZeroObject.object (C z : Set)
  requires zero : ZeroObject(C, z)
  shows z ∈ obj(C)
proof
  have initial := ZeroObject.initial with zero
  exact Initial.object with initial

-- The only endomorphism of a terminal or initial object is its identity.
theorem Terminal.endomorphism (C t f : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  requires fHom : f ∈ hom(C, t, t)
  shows f = id(C)(t)
proof
  have tInO := Terminal.object with terminal
  have idHom := hom.id with category, tInO
  exact Terminal.unique_morphism with terminal, tInO, fHom, idHom

theorem Initial.endomorphism (C i f : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  requires fHom : f ∈ hom(C, i, i)
  shows f = id(C)(i)
proof
  have iInO := Initial.object with initial
  have idHom := hom.id with category, iInO
  exact Initial.unique_morphism with initial, iInO, fHom, idHom

-- Terminal objects are isomorphic through a unique isomorphism.
theorem Terminal.inverse_pair (C t u f g : Set)
  requires category : Category(C)
  requires tTerminal : Terminal(C, t)
  requires uTerminal : Terminal(C, u)
  requires fHom : f ∈ hom(C, t, u)
  requires gHom : g ∈ hom(C, u, t)
  shows InversePair(C, f, g)
proof
  have gfHom := hom.comp with category, gHom, fHom
  have fgHom := hom.comp with category, fHom, gHom
  have gfId := Terminal.endomorphism with category, tTerminal, gfHom
  have fgId := Terminal.endomorphism with category, uTerminal, fgHom
  have fInM := hom.in_morphisms with fHom
  have gInM := hom.in_morphisms with gHom
  have domF := hom.dom with fHom
  have codF := hom.cod with fHom
  have domG := hom.dom with gHom
  have codG := hom.cod with gHom
  unfold InversePair
  refine ⟨fInM, gInM, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc

theorem Terminal.isomorphism (C t u f : Set)
  requires category : Category(C)
  requires tTerminal : Terminal(C, t)
  requires uTerminal : Terminal(C, u)
  requires fHom : f ∈ hom(C, t, u)
  shows Isomorphism(C, f)
proof
  have tInO := Terminal.object with tTerminal
  obtain ⟨g, gHom, unique⟩ := Terminal.exists_morphism with
    tTerminal, uTerminal.left
  have pair := Terminal.inverse_pair with
    category, tTerminal, uTerminal, fHom, gHom
  exact Isomorphism.of_pair with pair

theorem Terminal.isomorphic (C t u : Set)
  requires category : Category(C)
  requires tTerminal : Terminal(C, t)
  requires uTerminal : Terminal(C, u)
  shows Isomorphic(C, t, u)
proof
  have tInO := Terminal.object with tTerminal
  obtain ⟨f, fHom, unique⟩ := Terminal.exists_morphism with uTerminal, tInO
  have iso := Terminal.isomorphism with category, tTerminal, uTerminal, fHom
  exact Isomorphic.of_hom with fHom, iso

theorem Terminal.unique_isomorphism (C t u f g : Set)
  requires tTerminal : Terminal(C, t)
  requires uTerminal : Terminal(C, u)
  requires fHom : f ∈ hom(C, t, u)
  requires gHom : g ∈ hom(C, t, u)
  shows f = g
proof
  have tInO := Terminal.object with tTerminal
  exact Terminal.unique_morphism with uTerminal, tInO, fHom, gHom

theorem Initial.inverse_pair (C i j f g : Set)
  requires category : Category(C)
  requires iInitial : Initial(C, i)
  requires jInitial : Initial(C, j)
  requires fHom : f ∈ hom(C, i, j)
  requires gHom : g ∈ hom(C, j, i)
  shows InversePair(C, f, g)
proof
  have gfHom := hom.comp with category, gHom, fHom
  have fgHom := hom.comp with category, fHom, gHom
  have gfId := Initial.endomorphism with category, iInitial, gfHom
  have fgId := Initial.endomorphism with category, jInitial, fgHom
  have fInM := hom.in_morphisms with fHom
  have gInM := hom.in_morphisms with gHom
  have domF := hom.dom with fHom
  have codF := hom.cod with fHom
  have domG := hom.dom with gHom
  have codG := hom.cod with gHom
  unfold InversePair
  refine ⟨fInM, gInM, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc

theorem Initial.isomorphism (C i j f : Set)
  requires category : Category(C)
  requires iInitial : Initial(C, i)
  requires jInitial : Initial(C, j)
  requires fHom : f ∈ hom(C, i, j)
  shows Isomorphism(C, f)
proof
  have iInO := Initial.object with iInitial
  obtain ⟨g, gHom, unique⟩ := Initial.exists_morphism with jInitial, iInO
  have pair := Initial.inverse_pair with
    category, iInitial, jInitial, fHom, gHom
  exact Isomorphism.of_pair with pair

theorem Initial.isomorphic (C i j : Set)
  requires category : Category(C)
  requires iInitial : Initial(C, i)
  requires jInitial : Initial(C, j)
  shows Isomorphic(C, i, j)
proof
  have jInO := Initial.object with jInitial
  obtain ⟨f, fHom, unique⟩ := Initial.exists_morphism with iInitial, jInO
  have iso := Initial.isomorphism with category, iInitial, jInitial, fHom
  exact Isomorphic.of_hom with fHom, iso

theorem Initial.unique_isomorphism (C i j f g : Set)
  requires iInitial : Initial(C, i)
  requires jInitial : Initial(C, j)
  requires fHom : f ∈ hom(C, i, j)
  requires gHom : g ∈ hom(C, i, j)
  shows f = g
proof
  have jInO := Initial.object with jInitial
  exact Initial.unique_morphism with iInitial, jInO, fHom, gHom

theorem ZeroObject.isomorphic (C z w : Set)
  requires category : Category(C)
  requires zZero : ZeroObject(C, z)
  requires wZero : ZeroObject(C, w)
  shows Isomorphic(C, z, w)
proof
  have zTerminal := ZeroObject.terminal with zZero
  have wTerminal := ZeroObject.terminal with wZero
  exact Terminal.isomorphic with category, zTerminal, wTerminal

-- Being terminal or initial is invariant under isomorphism.
theorem Terminal.of_isomorphic (C t u : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  requires iso : Isomorphic(C, t, u)
  shows Terminal(C, u)
proof
  obtain ⟨f, fHom, g, pair⟩ := iso
  have gHom := InversePair.in_hom with pair, fHom
  have uInO := hom.cod with fHom
  have fInM := hom.in_morphisms with fHom
  have uIn : u ∈ obj(C)
    have codIn := Category.cod_closed with category, fInM
    rwa uInO at codIn
  unfold Terminal
  refine ⟨uIn, ?_⟩
  intros a aInO
  obtain ⟨v, vHom, unique⟩ := Terminal.exists_morphism with terminal, aInO
  have fvHom := hom.comp with category, fHom, vHom
  refine ⟨f ∘ v, fvHom, ?_⟩
  intros h hHom
  have ghHom := hom.comp with category, gHom, hHom
  have ghEqual := unique with g ∘ h, ghHom
  have assoc := Category.assoc_hom with category, fHom, gHom, hHom
  have unitH := Category.id_left_hom with category, hHom
  have fgId : f ∘ g = id(C)(u)
    have law := InversePair.right with pair
    have codF := hom.cod with fHom
    rwa codF at law
  calc
    h = id(C)(u) ∘ h := by rw unitH
    _ = (f ∘ g) ∘ h := by rw fgId
    _ = f ∘ (g ∘ h) := assoc
    _ = f ∘ v := by rw ghEqual

theorem Initial.of_isomorphic (C i j : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  requires iso : Isomorphic(C, i, j)
  shows Initial(C, j)
proof
  obtain ⟨f, fHom, g, pair⟩ := iso
  have gHom := InversePair.in_hom with pair, fHom
  have jInO := hom.cod with fHom
  have fInM := hom.in_morphisms with fHom
  have jIn : j ∈ obj(C)
    have codIn := Category.cod_closed with category, fInM
    rwa jInO at codIn
  unfold Initial
  refine ⟨jIn, ?_⟩
  intros a aInO
  obtain ⟨v, vHom, unique⟩ := Initial.exists_morphism with initial, aInO
  have vgHom := hom.comp with category, vHom, gHom
  refine ⟨v ∘ g, vgHom, ?_⟩
  intros h hHom
  have hfHom := hom.comp with category, hHom, fHom
  have hfEqual := unique with h ∘ f, hfHom
  have assoc := Category.assoc_hom with category, hHom, fHom, gHom
  have unitH := Category.id_right_hom with category, hHom
  have fgId : f ∘ g = id(C)(j)
    have law := InversePair.right with pair
    have codF := hom.cod with fHom
    rwa codF at law
  calc
    h = h ∘ id(C)(j) := by rw unitH
    _ = h ∘ (f ∘ g) := by rw fgId
    _ = (h ∘ f) ∘ g := by rw assoc
    _ = v ∘ g := by rw hfEqual

-- Every morphism into a terminal object is a split epimorphism when its
-- domain is itself terminal, and every morphism from a terminal object is
-- a split monomorphism.
theorem Terminal.split_mono (C t a f : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  requires fHom : f ∈ hom(C, t, a)
  shows SplitMonomorphism(C, f)
proof
  obtain ⟨r, rHom, unique⟩ := Terminal.exists_morphism with terminal, aInO
  have rfHom := hom.comp with category, rHom, fHom
  have rfId := Terminal.endomorphism with category, terminal, rfHom
  have fInM := hom.in_morphisms with fHom
  have rInM := hom.in_morphisms with rHom
  have domF := hom.dom with fHom
  have codF := hom.cod with fHom
  have domR := hom.dom with rHom
  have codR := hom.cod with rHom
  have retraction : Retraction(C, f, r)
    unfold Retraction
    refine ⟨fInM, rInM, ?_, ?_, ?_⟩
    . cc
    . cc
    . cc
  exact SplitMonomorphism.of_retraction with retraction

theorem Initial.split_epi (C i a f : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  requires fHom : f ∈ hom(C, a, i)
  shows SplitEpimorphism(C, f)
proof
  obtain ⟨s, sHom, unique⟩ := Initial.exists_morphism with initial, aInO
  have fsHom := hom.comp with category, fHom, sHom
  have fsId := Initial.endomorphism with category, initial, fsHom
  have fInM := hom.in_morphisms with fHom
  have sInM := hom.in_morphisms with sHom
  have domF := hom.dom with fHom
  have codF := hom.cod with fHom
  have domS := hom.dom with sHom
  have codS := hom.cod with sHom
  have section : SectionOf(C, f, s)
    unfold SectionOf
    refine ⟨fInM, sInM, ?_, ?_, ?_⟩
    . cc
    . cc
    . cc
  exact SplitEpimorphism.of_section with section

-- The unique morphism from an object to a terminal object, and from an
-- initial object to an object.
defunique terminalMorphism (C t a : Set)
    (f ∈ hom(C, a, t)) :=
  ∀ g ∈ hom(C, a, t), g = f
requires terminal : Terminal(C, t)
requires aInO : a ∈ obj(C)
proof
  exact Terminal.exists_morphism with terminal, aInO
uniqueness
  intros u hu first v hv second
  exact second with u, hu

theorem terminalMorphism.hom (C t a : Set)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  shows terminalMorphism(C, t, a) ∈ hom(C, a, t)
proof
  have selected := terminalMorphism.selected at C, t, a with
    terminal, aInO
  exact selected.left

theorem terminalMorphism.eq (C t a g : Set)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  requires gHom : g ∈ hom(C, a, t)
  shows g = terminalMorphism(C, t, a)
proof
  have selected := terminalMorphism.selected at C, t, a with
    terminal, aInO
  exact selected.right with g, gHom

theorem terminalMorphism.self (C t : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  shows terminalMorphism(C, t, t) = id(C)(t)
proof
  have tInO := Terminal.object with terminal
  have idHom := hom.id with category, tInO
  have equal := terminalMorphism.eq with terminal, tInO, idHom
  symm
  exact equal

theorem terminalMorphism.comp (C t a b f : Set)
  requires category : Category(C)
  requires terminal : Terminal(C, t)
  requires aInO : a ∈ obj(C)
  requires fHom : f ∈ hom(C, a, b)
  shows terminalMorphism(C, t, b) ∘ f =
    terminalMorphism(C, t, a)
proof
  have bInO : b ∈ obj(C)
    have fInM := hom.in_morphisms with fHom
    have codIn := Category.cod_closed with category, fInM
    have codF := hom.cod with fHom
    rwa codF at codIn
  have bHom := terminalMorphism.hom with terminal, bInO
  have composite := hom.comp with category, bHom, fHom
  exact terminalMorphism.eq with terminal, aInO, composite

defunique initialMorphism (C i a : Set)
    (f ∈ hom(C, i, a)) :=
  ∀ g ∈ hom(C, i, a), g = f
requires initial : Initial(C, i)
requires aInO : a ∈ obj(C)
proof
  exact Initial.exists_morphism with initial, aInO
uniqueness
  intros u hu first v hv second
  exact second with u, hu

theorem initialMorphism.hom (C i a : Set)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  shows initialMorphism(C, i, a) ∈ hom(C, i, a)
proof
  have selected := initialMorphism.selected at C, i, a with
    initial, aInO
  exact selected.left

theorem initialMorphism.eq (C i a g : Set)
  requires initial : Initial(C, i)
  requires aInO : a ∈ obj(C)
  requires gHom : g ∈ hom(C, i, a)
  shows g = initialMorphism(C, i, a)
proof
  have selected := initialMorphism.selected at C, i, a with
    initial, aInO
  exact selected.right with g, gHom

theorem initialMorphism.self (C i : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  shows initialMorphism(C, i, i) = id(C)(i)
proof
  have iInO := Initial.object with initial
  have idHom := hom.id with category, iInO
  have equal := initialMorphism.eq with initial, iInO, idHom
  symm
  exact equal

theorem initialMorphism.comp (C i a b f : Set)
  requires category : Category(C)
  requires initial : Initial(C, i)
  requires bInO : b ∈ obj(C)
  requires fHom : f ∈ hom(C, a, b)
  shows f ∘ initialMorphism(C, i, a) =
    initialMorphism(C, i, b)
proof
  have aInO : a ∈ obj(C)
    have fInM := hom.in_morphisms with fHom
    have domIn := Category.dom_closed with category, fInM
    have domF := hom.dom with fHom
    rwa domF at domIn
  have aHom := initialMorphism.hom with initial, aInO
  have composite := hom.comp with category, fHom, aHom
  exact initialMorphism.eq with initial, bInO, composite

-- In a category with a zero object, each hom-set has a zero morphism.
theorem ZeroObject.zero_morphism (C z a b : Set)
  requires category : Category(C)
  requires zero : ZeroObject(C, z)
  requires aInO : a ∈ obj(C)
  requires bInO : b ∈ obj(C)
  shows initialMorphism(C, z, b) ∘
    terminalMorphism(C, z, a) ∈ hom(C, a, b)
proof
  have initial := ZeroObject.initial with zero
  have terminal := ZeroObject.terminal with zero
  have toZero := terminalMorphism.hom with terminal, aInO
  have fromZero := initialMorphism.hom with initial, bInO
  exact hom.comp with category, fromZero, toZero