(** * Cofiber scale decomposition in semi-additive categories

    Given a semi-additive category with an adjunction Sigma -| Omega
    (suspension/loop, upsample/pool), the counit epsilon : Sigma Omega -> 1
    gives a "low-frequency projection" at each object.  When the connecting
    morphism in the cofiber of epsilon vanishes, X splits as a biproduct of
    its low-frequency part and its high-frequency residual.

    The splitting is natural in X: classification on cofibers is equivalent
    to multi-scale classification on the original features.

    The second section formalizes detection as pi0 of a presheaf colimit:
    connected components of locally-constant sections over a patch site.
*)

From HoTT Require Import Basics.Overture.
From HoTT.Categories Require Import
  Category.Core
  Functor.Core Functor.Composition.Core Functor.Identity
  NaturalTransformation.Core.
From HoTT.Categories.Additive Require Import ZeroObjects Biproducts SemiAdditive.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.
Local Open Scope morphism_scope.

(** * Pre-stable structure on a semi-additive category *)

Record PreStableData := {
  ps_cat : SemiAdditiveCategory;
  ps_Susp : Functor ps_cat ps_cat;
  ps_Loop : Functor ps_cat ps_cat;
  ps_epsilon : NaturalTransformation (ps_Susp o ps_Loop)%functor
                                     (Functor.Identity.identity ps_cat)
}.

Coercion ps_cat : PreStableData >-> SemiAdditiveCategory.

Section CofiberSplitting.

  Context (PS : PreStableData).

  Let C := ps_cat PS.
  Let Sig := ps_Susp PS.
  Let L := ps_Loop PS.
  Let eps := ps_epsilon PS.

  Definition low_freq (X : object C) : object C := Sig (L X).

  Definition eps_at (X : object C) : morphism C (low_freq X) X := eps X.

  (** A cofiber splitting of X along epsilon is a biproduct decomposition
      of X into low_freq X and some high-frequency complement H, mediated
      by an isomorphism between the biproduct object and X. *)

  Record CofiberSplitting (X : object C) := {
    cs_high : object C;
    cs_biprod : @Biproduct C _ (low_freq X) cs_high;
    cs_iso : morphism C (biproduct_obj (biproduct_data cs_biprod)) X;
    cs_iso_inv : morphism C X (biproduct_obj (biproduct_data cs_biprod));
    cs_sect : (cs_iso o cs_iso_inv = 1)%morphism;
    cs_retr : (cs_iso_inv o cs_iso = 1)%morphism;
    cs_eps_compat :
      (cs_iso o inl (biproduct_data cs_biprod) = eps_at X)%morphism
  }.

  Arguments cs_high {X} _.
  Arguments cs_biprod {X} _.
  Arguments cs_iso {X} _.
  Arguments cs_iso_inv {X} _.

  (** Naturality of epsilon. *)
  Lemma eps_natural {X Y : object C} (f : morphism C X Y)
    : (eps_at Y o (Sig _1 (L _1 f)) = f o eps_at X)%morphism.
  Proof.
    exact (commutes eps X Y f).
  Qed.

  (** The low-frequency component of a morphism. *)
  Definition low_component {X Y : object C} (f : morphism C X Y)
    : morphism C (low_freq X) (low_freq Y)
    := Sig _1 (L _1 f).

  (** The iso inverse composed with epsilon gives the left injection.
      Derivable from cs_eps_compat and cs_retr. *)
  Lemma iso_inv_eps (X : object C) (sp : CofiberSplitting X)
    : (cs_iso_inv sp o eps_at X
       = inl (biproduct_data (cs_biprod sp)))%morphism.
  Proof.
    rewrite <- (cs_eps_compat sp).
    rewrite <- associativity.
    rewrite (cs_retr sp).
    apply left_identity.
  Qed.

  (** ** Provable block structure

      Given a family of splittings and a morphism f : X -> Y, the
      conjugated morphism psi_Y o f o phi_X : BX -> BY has the
      following block structure with respect to the biproducts:

        - (low, low):  low_component f       [low_low_block]
        - (high, low): 0                      [cross_term_high_low_zero]
        - (low, high): requires cofiber       [cross_term_low_high_zero]
        - (high, high): requires cofiber

      The first two are provable from naturality of epsilon alone.
      The latter two require the splitting to be functorial. *)

  (** The conjugated morphism maps the low injection through epsilon's
      naturality to the low injection at the target. This is the key
      intermediate result used in both block theorems. *)
  Lemma conjugated_inl
    (split : forall X : object C, CofiberSplitting X)
    {X Y : object C} (f : morphism C X Y)
    : (cs_iso_inv (split Y) o f o cs_iso (split X)
        o inl (biproduct_data (cs_biprod (split X)))
       = inl (biproduct_data (cs_biprod (split Y)))
        o low_component f)%morphism.
  Proof.
    repeat rewrite Category.Core.associativity.
    rewrite (cs_eps_compat (split X)).
    rewrite <- (eps_natural f).
    assert (H : (cs_iso_inv (split Y) o (eps_at Y o low_component f)
                 = (cs_iso_inv (split Y) o eps_at Y) o low_component f)%morphism).
    { symmetry. apply Category.Core.associativity. }
    rewrite H.
    rewrite (iso_inv_eps (split Y)).
    reflexivity.
  Qed.

  (** The low-low block equals the functorial low-frequency component. *)
  Theorem low_low_block
    (split : forall X : object C, CofiberSplitting X)
    {X Y : object C} (f : morphism C X Y)
    : let BX := biproduct_data (cs_biprod (split X)) in
      let BY := biproduct_data (cs_biprod (split Y)) in
      (outl BY o cs_iso_inv (split Y) o f o cs_iso (split X) o inl BX
       = low_component f)%morphism.
  Proof.
    intros BX BY.
    repeat rewrite Category.Core.associativity.
    assert (H := conjugated_inl split f).
    repeat rewrite Category.Core.associativity in H.
    rewrite H.
    rewrite <- Category.Core.associativity.
    rewrite (beta_l (biproduct_is (cs_biprod (split Y)))).
    apply left_identity.
  Qed.

  (** The high-low cross term vanishes: injecting from the low-frequency
      part of X and projecting onto the high-frequency part of Y gives
      zero. Follows from naturality of epsilon and the biproduct axioms. *)
  Theorem cross_term_high_low_zero
    (split : forall X : object C, CofiberSplitting X)
    {X Y : object C} (f : morphism C X Y)
    : let BX := biproduct_data (cs_biprod (split X)) in
      let BY := biproduct_data (cs_biprod (split Y)) in
      (outr BY o cs_iso_inv (split Y) o f o cs_iso (split X) o inl BX
       = @zero_morphism C _ (low_freq X) (cs_high (split Y)))%morphism.
  Proof.
    intros BX BY.
    repeat rewrite Category.Core.associativity.
    assert (H := conjugated_inl split f).
    repeat rewrite Category.Core.associativity in H.
    rewrite H.
    rewrite <- Category.Core.associativity.
    rewrite (mixed_r (biproduct_is (cs_biprod (split Y)))).
    apply zero_morphism_left.
  Qed.

  (** The low-high cross term vanishes when the splitting is functorial:
      the conjugated morphism maps the high-frequency injection at X
      into the high-frequency injection at Y.

      This condition is derivable when the splitting comes from a
      cofiber construction (distinguished triangles + vanishing
      connecting morphism), which requires the stable category
      machinery from PR 2288. Here we take it as a hypothesis. *)
  Theorem cross_term_low_high_zero
    (split : forall X : object C, CofiberSplitting X)
    {X Y : object C} (f : morphism C X Y)
    (f_high : morphism C (cs_high (split X)) (cs_high (split Y)))
    (H_func :
      (cs_iso_inv (split Y) o f o cs_iso (split X)
        o inr (biproduct_data (cs_biprod (split X)))
       = inr (biproduct_data (cs_biprod (split Y))) o f_high)%morphism)
    : let BX := biproduct_data (cs_biprod (split X)) in
      let BY := biproduct_data (cs_biprod (split Y)) in
      (outl BY o cs_iso_inv (split Y) o f o cs_iso (split X) o inr BX
       = @zero_morphism C _ (cs_high (split X)) (low_freq Y))%morphism.
  Proof.
    intros BX BY.
    repeat rewrite associativity.
    repeat rewrite associativity in H_func.
    rewrite H_func.
    rewrite <- associativity.
    rewrite (mixed_l (biproduct_is (cs_biprod (split Y)))).
    apply zero_morphism_left.
  Qed.

  (** ** Iterated decomposition *)

  Fixpoint iterated_low (n : nat) (X : object C) : object C :=
    match n with
    | O => X
    | S m => low_freq (iterated_low m X)
    end.

  Definition scale_band
    (split : forall X, CofiberSplitting X) (k : nat) (X : object C)
    : object C :=
    cs_high (split (iterated_low k X)).

  Definition iterated_splitting
    (split : forall X, CofiberSplitting X) (k : nat) (X : object C)
    : CofiberSplitting (iterated_low k X) :=
    split (iterated_low k X).

End CofiberSplitting.

(** * Detection as pi0 of a presheaf colimit *)

From HoTT Require Import Basics.Trunc Truncations.Core.
From HoTT Require Import Diagrams.Graph Diagrams.Diagram.
From HoTT Require Import Colimits.Colimit.

Section SheafPi0.

  Context (Site : Graph).
  Context (F : Diagram Site).

  Definition presheaf_colimit : Type := Colimit F.

  Definition pi0 : Type := Trunc 0 presheaf_colimit.

  Global Instance ishset_pi0 : IsHSet pi0 := _.

  Definition pi0_in (i : Site) (x : obj F i) : pi0 := tr (colim i x).

  Definition same_component (i j : Site) (x : obj F i) (y : obj F j)
    : Type :=
    pi0_in i x = pi0_in j y.

  Record FinitePresentation := {
    fp_graph : Graph;
    fp_diagram : Diagram fp_graph;
    fp_n_gen : nat;
    fp_n_rel : nat;
    fp_equiv : Colimit fp_diagram <~> Colimit F
  }.

  Theorem finite_presentation_pi0 (P : FinitePresentation)
    : Trunc 0 (Colimit (fp_diagram P)) <~> pi0.
  Proof.
    apply Trunc_functor_equiv.
    exact (fp_equiv P).
  Defined.

End SheafPi0.