-- Functors between small categories
-- 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.Functor
import Terminal

-- A functor is a structure of its object map, its morphism map, and its
-- source and target categories. Under a hypothesis F : C ⥤ D the values
-- F.obj(a) and F.map(f) are written F(a) and F(f): the elaborator reads off
-- whether the argument is an object or a morphism of C. Functor(F, C, D),
-- written F : C ⥤ D, says that the source and target of F are the
-- categories C and D, that the object map sends C.obj to D.obj and the
-- morphism map C.mor to D.mor, and that the maps preserve endpoints,
-- identities, and composition.
structure Functor (C D : Set)
  | obj map src tgt : Set
  where
    source_category : Category(C)
    target_category : Category(D)
    objects : obj : C.obj → D.obj
    morphisms : map : C.mor → D.mor
    homs : ∀ (a b ∈ C.obj) (f : a ⟶ b), map(f) : obj(a) ⟶ obj(b)
    identities : ∀ a ∈ C.obj, map(C.id(a)) = D.id(obj(a))
    composites : ∀ (a b c ∈ C.obj) (f : a ⟶ b) (g : b ⟶ c),
      map(g ∘ f) = map(g) ∘ map(f)
    source : src = C
    target : tgt = D

tactic functor_projections := simp [Functor.mk.obj, Functor.mk.map, Functor.mk.src, Functor.mk.tgt]

-- A functor hypothesis is a transparent guard, and it supplies both
-- compositions and both arrows: g ∘ f for morphisms of the source, F(g) ∘
-- F(f) for morphisms of the target, f : a ⟶ b for objects of C, and
-- F(f) : F(a) ⟶ F(b) in D.
notation guard "_ : _ ⥤ _" => Functor
notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Functor(F, C, D) for C.mor
notation infixr 70 "∘" => call2(D.comp, _, _) via hypothesis Functor(F, C, D) for D.mor
notation mixfix "_ : _ ⟶ _" => Morphism(C, _, _, _) via hypothesis Functor(F, C, D) for C.obj, C.mor
notation mixfix "_ : _ ⟶ _" => Morphism(D, _, _, _) via hypothesis Functor(F, C, D) for D.obj, D.mor

-- Faithful: injective on each hom-set. Full: surjective onto each hom-set
-- between images.
predicate Faithful (F C D : Set) :=
  Functor(F, C, D) ∧ (∀ (a b ∈ obj(C)) (f g : a ⟶ b), F(f) = F(g) → f = g)

predicate Full (F C D : Set) :=
  Functor(F, C, D) ∧ (∀ (a b ∈ obj(C)) (h : F(a) ⟶ F(b)), ∃ (f : a ⟶ b), F(f) = h)

section FunctorLaws
variable (F C D : Set)
hypothesis functor : F : C ⥤ D

theorem Functor.source
  shows src(F) = C
proof
  obtain ⟨shape, source, target, objects, morphisms, homs, identities,
    composites, srcF, tgtF⟩ := functor
  exact srcF

theorem Functor.target
  shows tgt(F) = D
proof
  obtain ⟨shape, source, target, objects, morphisms, homs, identities,
    composites, srcF, tgtF⟩ := functor
  exact tgtF

theorem Functor.source_category
  shows Category(C)
proof
  obtain ⟨shape, source, rest⟩ := functor
  exact source

theorem Functor.target_category
  shows Category(D)
proof
  obtain ⟨shape, source, target, rest⟩ := functor
  exact target

theorem Functor.data
  shows Functor.Data(F)
proof
  obtain ⟨shape, rest⟩ := functor
  exact shape

theorem Functor.self
  shows Functor(F, src(F), tgt(F))
proof
  have srcF := Functor.source with functor
  have tgtF := Functor.target with functor
  rw [srcF, tgtF]
  exact functor

theorem Functor.object_function
  shows obj(F) : obj(C) → obj(D)
proof
  obtain ⟨shape, source, target, objects, rest⟩ := functor
  exact objects

theorem Functor.morphism_function
  shows map(F) : mor(C) → mor(D)
proof
  obtain ⟨shape, source, target, objects, morphisms, rest⟩ := functor
  exact morphisms

theorem Functor.object_closed (a : Set)
  requires aInO : a ∈ obj(C)
  shows F(a) ∈ obj(D)
proof
  have function := Functor.object_function with functor
  exact FunctionBetween.apply_closed with function, aInO

theorem Functor.morphism_closed (f : Set)
  requires fInM : f ∈ mor(C)
  shows F(f) ∈ mor(D)
proof
  have function := Functor.morphism_function with functor
  exact FunctionBetween.apply_closed with function, fInM

-- The functor laws on hom-typed binders.
instance Functor.map_hom (a b ∈ obj(C)) (f : a ⟶ b)
  shows F(f) : F(a) ⟶ F(b)
proof
  obtain ⟨shape, source, target, objects, morphisms, homs, rest⟩ := functor
  exact homs with a, assumption, b, assumption, f, assumption

theorem Functor.map_id (a : Set)
  requires aInO : a ∈ obj(C)
  shows F(id(C)(a)) = id(D)(F(a))
proof
  obtain ⟨shape, source, target, objects, morphisms, homs, identities, rest⟩ := functor
  exact identities with a, aInO

theorem Functor.map_comp (a b c ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ c)
  shows F(g ∘ f) = F(g) ∘ F(f)
proof
  obtain ⟨shape, source, target, objects, morphisms, homs, identities,
    composites, rest⟩ := functor
  exact composites with a, assumption, b, assumption, c, assumption, f, assumption, g, assumption

-- The same laws on bare morphisms and on hom-sets.
theorem Functor.dom (f : Set)
  requires fInM : f ∈ mor(C)
  shows dom(D)(F(f)) = F(dom(C)(f))
proof
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have image : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *
  cc

theorem Functor.cod (f : Set)
  requires fInM : f ∈ mor(C)
  shows cod(D)(F(f)) = F(cod(C)(f))
proof
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have image : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *
  cc

theorem Functor.comp (g f : Set)
  requires gInM : g ∈ mor(C)
  requires fInM : f ∈ mor(C)
  requires composable : dom(C)(g) = cod(C)(f)
  shows F(g ∘ f) = F(g) ∘ F(f)
proof
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *
  exact Functor.map_comp with *

theorem Functor.composable (g f : Set)
  requires gInM : g ∈ mor(C)
  requires fInM : f ∈ mor(C)
  requires composable : dom(C)(g) = cod(C)(f)
  shows dom(D)(F(g)) = cod(D)(F(f))
proof
  have domG := Functor.dom with functor, gInM
  have codF := Functor.cod with functor, fInM
  cc

theorem Functor.hom (a b f : Set)
  requires fHom : f ∈ hom(C, a, b)
  shows F(f) ∈ hom(D, F(a), F(b))
proof
  have typed : f : a ⟶ b := Morphism.of_hom with fHom
  have image : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *
  exact Morphism.hom with image

-- Functors preserve commutative triangles and squares.
theorem Functor.triangle (a b c ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ c) (h : a ⟶ c)
  requires commutes : g ∘ f = h
  shows F(g) ∘ F(f) = F(h)
proof
  calc
    F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp
    _ = F(h) := by rw commutes

theorem Functor.square (a b c d ∈ obj(C)) (f : a ⟶ b) (g : b ⟶ d) (h : a ⟶ c) (k : c ⟶ d)
  requires commutes : g ∘ f = k ∘ h
  shows F(g) ∘ F(f) = F(k) ∘ F(h)
proof
  calc
    F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp
    _ = F(k ∘ h) := by rw commutes
    _ = F(k) ∘ F(h) := by rw Functor.map_comp

-- Functors preserve inverse pairs, isomorphisms, retractions, and sections.
theorem Functor.inverse_pair (f g : Set)
  requires pair : InversePair(C, f, g)
  shows InversePair(D, F(f), F(g))
proof
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := InversePair.hom with *
  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with *
  have gf : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with pair
  have fg : f ∘ g = id(C)(cod(C)(f)) := InversePair.right with pair
  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *
  have gImage : F(g) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *
  unfold InversePair
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc
  . calc
      F(g) ∘ F(f) = F(g ∘ f) := by rw Functor.map_comp
      _ = F(id(C)(dom(C)(f))) := by rw gf
      _ = id(D)(F(dom(C)(f))) := by rw Functor.map_id
      _ = id(D)(dom(D)(F(f))) := by cc
  . calc
      F(f) ∘ F(g) = F(f ∘ g) := by rw Functor.map_comp
      _ = F(id(C)(cod(C)(f))) := by rw fg
      _ = id(D)(F(cod(C)(f))) := by rw Functor.map_id
      _ = id(D)(cod(D)(F(f))) := by cc

theorem Functor.isomorphism (f : Set)
  requires iso : Isomorphism(C, f)
  shows Isomorphism(D, F(f))
proof
  obtain ⟨g, pair⟩ := iso
  have image := Functor.inverse_pair with functor, pair
  exact Isomorphism.of_pair with image

theorem Functor.isomorphic (a b : Set)
  requires iso : Isomorphic(C, a, b)
  shows Isomorphic(D, F(a), F(b))
proof
  obtain ⟨f, fHom, fIso⟩ := iso
  have imageHom := Functor.hom with functor, fHom
  have imageIso := Functor.isomorphism with functor, fIso
  exact Isomorphic.of_hom with imageHom, imageIso

theorem Functor.retraction (f r : Set)
  requires retraction : Retraction(C, f, r)
  shows Retraction(D, F(f), F(r))
proof
  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have rHom : r : cod(C)(f) ⟶ dom(C)(f) := Morphism.of_dom_cod with *
  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *
  have rImage : F(r) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *
  unfold Retraction
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc
  . calc
      F(r) ∘ F(f) = F(r ∘ f) := by rw Functor.map_comp
      _ = F(id(C)(dom(C)(f))) := by rw law
      _ = id(D)(F(dom(C)(f))) := by rw Functor.map_id
      _ = id(D)(dom(D)(F(f))) := by cc

theorem Functor.section (f s : Set)
  requires section : SectionOf(C, f, s)
  shows SectionOf(D, F(f), F(s))
proof
  obtain ⟨fInM, sInM, domS, codS, law⟩ := section
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have sHom : s : cod(C)(f) ⟶ dom(C)(f) := Morphism.of_dom_cod with *
  have fImage : F(f) : F(dom(C)(f)) ⟶ F(cod(C)(f)) := Functor.map_hom with *
  have sImage : F(s) : F(cod(C)(f)) ⟶ F(dom(C)(f)) := Functor.map_hom with *
  unfold SectionOf
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc
  . calc
      F(f) ∘ F(s) = F(f ∘ s) := by rw Functor.map_comp
      _ = F(id(C)(cod(C)(f))) := by rw law
      _ = id(D)(F(cod(C)(f))) := by rw Functor.map_id
      _ = id(D)(cod(D)(F(f))) := by cc

theorem Functor.split_mono (f : Set)
  requires split : SplitMonomorphism(C, f)
  shows SplitMonomorphism(D, F(f))
proof
  obtain ⟨r, retraction⟩ := split
  have image := Functor.retraction with functor, retraction
  exact SplitMonomorphism.of_retraction with image

theorem Functor.split_epi (f : Set)
  requires split : SplitEpimorphism(C, f)
  shows SplitEpimorphism(D, F(f))
proof
  obtain ⟨s, section⟩ := split
  have image := Functor.section with functor, section
  exact SplitEpimorphism.of_section with image

end FunctorLaws

-- Faithful and full functors.
theorem Faithful.functor (F C D : Set)
  requires faithful : Faithful(F, C, D)
  shows F : C ⥤ D
proof
  obtain ⟨functor, cancel⟩ := faithful
  exact functor

theorem Full.functor (F C D : Set)
  requires full : Full(F, C, D)
  shows F : C ⥤ D
proof
  obtain ⟨functor, lift⟩ := full
  exact functor

section FullFaithful
variable (F C D : Set)
hypothesis functor : F : C ⥤ D

theorem Faithful.cancel (a b ∈ obj(C)) (f g : a ⟶ b)
  requires faithful : Faithful(F, C, D)
  requires sameImage : F(f) = F(g)
  shows f = g
proof
  obtain ⟨functorF, cancel⟩ := faithful
  exact cancel with a, assumption, b, assumption, f, assumption, g, assumption, sameImage

theorem Full.lift (a b ∈ obj(C)) (h : F(a) ⟶ F(b))
  requires full : Full(F, C, D)
  shows ∃ (f : a ⟶ b), F(f) = h
proof
  obtain ⟨functorF, lift⟩ := full
  exact lift with a, assumption, b, assumption, h, assumption

end FullFaithful

-- The identity functor.
def identityFunctor (C : Set) : Set :=
  Functor.mk(identity(Category.obj(C)), identity(Category.mor(C)), C, C)

theorem identityFunctor.obj (C a : Set)
  requires aInO : a ∈ Category.obj(C)
  shows obj(identityFunctor(C))(a) = a
proof
  have value := identity.apply with aInO
  simp [identityFunctor, Functor.mk.obj, value]

theorem identityFunctor.map (C f : Set)
  requires fInM : f ∈ Category.mor(C)
  shows map(identityFunctor(C))(f) = f
proof
  have value := identity.apply with fInM
  simp [identityFunctor, Functor.mk.map, value]

theorem identityFunctor.src (C : Set)
  shows src(identityFunctor(C)) = C
proof
  unfold identityFunctor
  exact Functor.mk.src at identity(Category.obj(C)), identity(Category.mor(C)), C, C

theorem identityFunctor.tgt (C : Set)
  shows tgt(identityFunctor(C)) = C
proof
  unfold identityFunctor
  exact Functor.mk.tgt at identity(Category.obj(C)), identity(Category.mor(C)), C, C

theorem identityFunctor.object_function (C : Set)
  shows obj(identityFunctor(C)) : Category.obj(C) → Category.obj(C)
proof
  unfold identityFunctor
  rw Functor.mk.obj
  exact identity.function at Category.obj(C)

theorem identityFunctor.morphism_function (C : Set)
  shows map(identityFunctor(C)) : Category.mor(C) → Category.mor(C)
proof
  unfold identityFunctor
  rw Functor.mk.map
  exact identity.function at Category.mor(C)

section IdentityFunctor
variable (C : Set)
hypothesis category : Category(C)

theorem Functor.identity
  shows identityFunctor(C) : C ⥤ C
proof
  have objects := identity.function at obj(C)
  have morphisms := identity.function at mor(C)
  unfold identityFunctor
  apply Functor.intro with category, category, objects, morphisms
  . intros a aIn b bIn f fHom
    simpa [identity.apply] using fHom
  . intros a aIn
    simp [identity.apply]
  . intros a aIn b bIn c cIn f fHom g gHom
    simp [identity.apply]
  . rfl
  . rfl

theorem Faithful.identity
  shows Faithful(identityFunctor(C), C, C)
proof
  have functor := Functor.identity with category
  unfold Faithful
  refine ⟨functor, ?_⟩
  intros a aIn b bIn f fHom g gHom same
  simp [identityFunctor.map] at same
  exact same

theorem Full.identity
  shows Full(identityFunctor(C), C, C)
proof
  have functor := Functor.identity with category
  unfold Full
  refine ⟨functor, ?_⟩
  intros a aIn b bIn h hHom
  simp [identityFunctor.obj] at hHom
  refine ⟨h, hHom, ?_⟩
  simp [identityFunctor.map]

end IdentityFunctor

-- Composition of functors, written F ⋙ G for F followed by G.
def composeFunctor (F G : Set) : Set :=
  Functor.mk(
    compose(Functor.obj(G), Functor.obj(F),
      Category.obj(src(F)), Category.obj(tgt(F)), Category.obj(tgt(G))),
    compose(Functor.map(G), Functor.map(F), mor(src(F)), mor(tgt(F)), mor(tgt(G))),
    src(F), tgt(G))

notation infixl 80 "⋙" => composeFunctor

section FunctorComposition
variable (F G C D E : Set)
hypothesis functorF : F : C ⥤ D
hypothesis functorG : G : D ⥤ E

theorem composeFunctor.src
  shows src(F ⋙ G) = C
proof
  have srcF := Functor.source with functorF
  simp [composeFunctor, Functor.mk.src, srcF]

theorem composeFunctor.tgt
  shows tgt(F ⋙ G) = E
proof
  have tgtG := Functor.target with functorG
  simp [composeFunctor, Functor.mk.tgt, tgtG]

theorem composeFunctor.object_function
  shows obj(F ⋙ G) : obj(C) → obj(E)
proof
  have srcF := Functor.source with functorF
  have tgtF := Functor.target with functorF
  have tgtG := Functor.target with functorG
  have objectsF := Functor.object_function with functorF
  have objectsG := Functor.object_function with functorG
  have composed := compose.function with objectsF, objectsG
  unfold composeFunctor
  rw [Functor.mk.obj, srcF, tgtF, tgtG]
  exact composed

theorem composeFunctor.morphism_function
  shows map(F ⋙ G) : mor(C) → mor(E)
proof
  have srcF := Functor.source with functorF
  have tgtF := Functor.target with functorF
  have tgtG := Functor.target with functorG
  have morphismsF := Functor.morphism_function with functorF
  have morphismsG := Functor.morphism_function with functorG
  have composed := compose.function with morphismsF, morphismsG
  unfold composeFunctor
  rw [Functor.mk.map, srcF, tgtF, tgtG]
  exact composed

theorem composeFunctor.obj_apply (a : Set)
  requires aInO : a ∈ obj(C)
  shows obj(F ⋙ G)(a) = G(F(a))
proof
  have srcF := Functor.source with functorF
  have tgtF := Functor.target with functorF
  have tgtG := Functor.target with functorG
  have objectsF := Functor.object_function with functorF
  have objectsG := Functor.object_function with functorG
  have value := compose.apply with objectsF, objectsG, aInO
  simp [composeFunctor, Functor.mk.obj, srcF, tgtF, tgtG, value]

theorem composeFunctor.map_apply (f : Set)
  requires fInM : f ∈ mor(C)
  shows map(F ⋙ G)(f) = G(F(f))
proof
  have srcF := Functor.source with functorF
  have tgtF := Functor.target with functorF
  have tgtG := Functor.target with functorG
  have morphismsF := Functor.morphism_function with functorF
  have morphismsG := Functor.morphism_function with functorG
  have value := compose.apply with morphismsF, morphismsG, fInM
  simp [composeFunctor, Functor.mk.map, srcF, tgtF, tgtG, value]

-- The data of the composite: its shape, its categories, its two maps, and
-- its source and target, in the order the Functor predicate lists them.
theorem composeFunctor.data
  shows Functor.Data(F ⋙ G) ∧ Category(C) ∧ Category(E) ∧
    (obj(F ⋙ G) : obj(C) → obj(E)) ∧ (map(F ⋙ G) : mor(C) → mor(E)) ∧
    src(F ⋙ G) = C ∧ tgt(F ⋙ G) = E
proof
  have shape : Functor.Data(F ⋙ G) by simp [composeFunctor, Functor.mk.data]
  have source := Functor.source_category with functorF
  have target := Functor.target_category with functorG
  have objects : obj(F ⋙ G) : obj(C) → obj(E) := composeFunctor.object_function with *
  have morphisms : map(F ⋙ G) : mor(C) → mor(E) := composeFunctor.morphism_function with *
  have srcLaw : src(F ⋙ G) = C := composeFunctor.src with *
  have tgtLaw : tgt(F ⋙ G) = E := composeFunctor.tgt with *
  refine ⟨shape, source, target, objects, morphisms, srcLaw, tgtLaw⟩

theorem Functor.compose
  shows F ⋙ G : C ⥤ E
proof
  obtain ⟨shape, source, target, objects, morphisms, srcLaw, tgtLaw⟩ :=
    composeFunctor.data with functorF, functorG
  unfold Functor
  refine ⟨shape, source, target, objects, morphisms, ?_, ?_, ?_, srcLaw, tgtLaw⟩
  . intros a aIn b bIn f fHom
    simp [composeFunctor.obj_apply, composeFunctor.map_apply]
  . intros a aIn
    simp [composeFunctor.obj_apply, composeFunctor.map_apply, Functor.map_id]
  . intros a aIn b bIn c cIn f fHom g gHom
    simp [composeFunctor.obj_apply, composeFunctor.map_apply, Functor.map_comp]

-- Faithful functors compose, and so do full functors.
theorem Faithful.compose
  requires faithfulF : Faithful(F, C, D)
  requires faithfulG : Faithful(G, D, E)
  shows Faithful(F ⋙ G, C, E)
proof
  have functor := Functor.compose with functorF, functorG
  unfold Faithful
  refine ⟨functor, ?_⟩
  intros a aIn b bIn f fHom g gHom same
  simp [composeFunctor.map_apply] at same
  have aImage := Functor.object_closed with functorF, aIn
  have bImage := Functor.object_closed with functorF, bIn
  have fImage : F(f) : F(a) ⟶ F(b) := Functor.map_hom with *
  have gImage : F(g) : F(a) ⟶ F(b) := Functor.map_hom with *
  have innerSame : F(f) = F(g) := Faithful.cancel with
    aImage, bImage, fImage, gImage, functorG, faithfulG, same
  exact Faithful.cancel with aIn, bIn, fHom, gHom, functorF, faithfulF, innerSame

theorem Full.compose
  requires fullF : Full(F, C, D)
  requires fullG : Full(G, D, E)
  shows Full(F ⋙ G, C, E)
proof
  have functor := Functor.compose with functorF, functorG
  unfold Full
  refine ⟨functor, ?_⟩
  intros a aIn b bIn h hHom
  have aImage := Functor.object_closed with functorF, aIn
  have bImage := Functor.object_closed with functorF, bIn
  have objA := composeFunctor.obj_apply with functorF, functorG, aIn
  have objB := composeFunctor.obj_apply with functorF, functorG, bIn
  rw [objA, objB] at hHom
  obtain ⟨k, kHom, kImage⟩ := Full.lift with aImage, bImage, hHom, functorG, fullG
  obtain ⟨f, fHom, fImage⟩ := Full.lift with aIn, bIn, kHom, functorF, fullF
  refine ⟨f, fHom, ?_⟩
  simp [composeFunctor.map_apply, fImage, kImage]

end FunctorComposition