NormalImage.lean

theorem nonempty_terminal_hom_iff_exists_range_fixed
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) (X : C) :
    Nonempty (⊤_ C' ⟶ H.obj X) ↔
      ∃ x : F.obj X,
        ∀ a : Aut F', autHomOfCompIso H t a • x = x

theorem terminal_decomposition_of_range_trivial
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) (X : C)
    (htriv : ∀ (a : Aut F') (x : F.obj X),
      autHomOfCompIso H t a • x = x) :
    ∃ (ι : Type) (_ : Finite ι),
      Nonempty ((∐ fun _ : ι => ⊤_ C') ≅ H.obj X) := by
  apply
    (exists_iso_finite_coproduct_terminal_iff_fixed
      (F'' := F') (H.obj X)).2
  intro a y
  apply (ConcreteCategory.bijective_of_isIso (t.app X).hom).injective
  let s := (functorToContActionCompIso H t).app X
  have hs := ConcreteCategory.congr_hom (s.hom.hom.comm a) y
  change (t.app X).hom (a • y) =
    autHomOfCompIso H t a • (t.app X).hom y at hs
  calc
    (t.app X).hom (a • y) =
        autHomOfCompIso H t a • (t.app X).hom y := hs
    _ = (t.app X).hom y := htriv a ((t.app X).hom y)

theorem range_trivial_of_terminal_decomposition
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) (X : C)
    (hdecomp : ∃ (ι : Type) (_ : Finite ι),
      Nonempty ((∐ fun _ : ι => ⊤_ C') ≅ H.obj X)) :
    ∀ (a : Aut F') (x : F.obj X),
      autHomOfCompIso H t a • x = x := by
  intro a x
  let y : F'.obj (H.obj X) := (t.app X).inv x
  have hxy : (t.app X).hom y = x :=
    FintypeCat.inv_hom_id_apply (t.app X) x
  have hy : a • y = y :=
    (exists_iso_finite_coproduct_terminal_iff_fixed
      (F'' := F') (H.obj X)).1 hdecomp a y
  let s := (functorToContActionCompIso H t).app X
  have hs := ConcreteCategory.congr_hom (s.hom.hom.comm a) y
  change (t.app X).hom (a • y) =
    autHomOfCompIso H t a • (t.app X).hom y at hs
  calc
    autHomOfCompIso H t a • x =
        autHomOfCompIso H t a • (t.app X).hom y := congrArg _ hxy.symm
    _ = (t.app X).hom (a • y) := hs.symm
    _ = (t.app X).hom y := congrArg _ hy
    _ = x := hxy

theorem autHomOfCompIso_range_normal_iff_terminal_decomposition
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) :
    (autHomOfCompIso H t).toMonoidHom.range.Normal ↔
      ∀ X : C, IsConnected X →
        Nonempty (⊤_ C' ⟶ H.obj X) →
        ∃ (ι : Type) (_ : Finite ι),
          Nonempty ((∐ fun _ : ι => ⊤_ C') ≅ H.obj X) := by
  constructor
  · intro hnormal X hconn hpoint
    let : IsConnected X := hconn
    let E := functorToContAction F
    have htrans :
        MulAction.IsPretransitive (Aut F) (E.obj X).obj.V := by
      change MulAction.IsPretransitive (Aut F) (F.obj X)
      infer_instance
    have hfixed :
        ∃ x : (E.obj X).obj.V,
          ∀ a : Aut F', autHomOfCompIso H t a • x = x :=
      (nonempty_terminal_hom_iff_exists_range_fixed H t X).1 hpoint
    have htriv :
        ∀ (a : Aut F') (x : (E.obj X).obj.V),
          autHomOfCompIso H t a • x = x :=
      (ContAction.range_normal_iff_fixed_point_implies_trivial
        (autHomOfCompIso H t)).1 hnormal (E.obj X) htrans hfixed
    exact terminal_decomposition_of_range_trivial H t X htriv
  · intro hdecomp
    apply
      (ContAction.range_normal_iff_fixed_point_implies_trivial
        (autHomOfCompIso H t)).2
    intro Z htrans hfixed
    let : MulAction (Aut F) Z.obj.V := Action.instMulAction Z.obj
    let E := functorToContAction F
    let X : C := E.objPreimage Z
    let eZ : E.obj X ≅ Z := E.objObjPreimageIso Z
    let ef :=
      (forget₂ (ContAction FintypeCat (Aut F)) FintypeCat).mapIso eZ
    let z : Z.obj.V := hfixed.choose
    let x : F.obj X := ef.inv z
    have hxz : ef.hom x = z :=
      FintypeCat.inv_hom_id_apply ef z
    let : Nonempty (F.obj X) := ⟨x⟩
    let : MulAction.IsPretransitive (Aut F) (F.obj X) := by
      constructor
      intro x₁ x₂
      let z₁ : Z.obj.V := ef.hom x₁
      let z₂ : Z.obj.V := ef.hom x₂
      obtain ⟨a, ha⟩ := htrans.exists_smul_eq z₁ z₂
      refine ⟨a, ?_⟩
      apply (ConcreteCategory.bijective_of_isIso ef.hom).injective
      have hc := ConcreteCategory.congr_hom (eZ.hom.hom.comm a) x₁
      change ef.hom (a • x₁) = a • z₁ at hc
      exact hc.trans ha
    let : IsConnected X :=
      FiberFunctor.isConnected_of_isPretransitive F X
    have hfixedX :
        ∃ x : F.obj X,
          ∀ a : Aut F', autHomOfCompIso H t a • x = x := by
      refine ⟨x, ?_⟩
      intro a
      apply (ConcreteCategory.bijective_of_isIso ef.hom).injective
      have hc := ConcreteCategory.congr_hom
        (eZ.hom.hom.comm (autHomOfCompIso H t a)) x
      change ef.hom (autHomOfCompIso H t a • x) =
        (Z.obj.ρ (autHomOfCompIso H t a)).hom (ef.hom x) at hc
      have hz := hfixed.choose_spec a
      change (Z.obj.ρ (autHomOfCompIso H t a)).hom z = z at hz
      exact hc.trans <|
        (congrArg
          (fun y : Z.obj.V =>
            (Z.obj.ρ (autHomOfCompIso H t a)).hom y) hxz).trans <|
        hz.trans hxz.symm
    have hpoint : Nonempty (⊤_ C' ⟶ H.obj X) :=
      (nonempty_terminal_hom_iff_exists_range_fixed H t X).2 hfixedX
    have htrivX :
        ∀ (a : Aut F') (x : F.obj X),
          autHomOfCompIso H t a • x = x :=
      range_trivial_of_terminal_decomposition H t X
        (hdecomp X inferInstance hpoint)
    intro a z'
    let x' : F.obj X := ef.inv z'
    have hxz' : ef.hom x' = z' :=
      FintypeCat.inv_hom_id_apply ef z'
    have hc := ConcreteCategory.congr_hom
      (eZ.hom.hom.comm (autHomOfCompIso H t a)) x'
    change ef.hom (autHomOfCompIso H t a • x') =
      (Z.obj.ρ (autHomOfCompIso H t a)).hom (ef.hom x') at hc
    change
      (Z.obj.ρ (autHomOfCompIso H t a)).hom z' = z'
    exact
      (congrArg
        (fun y : Z.obj.V =>
          (Z.obj.ρ (autHomOfCompIso H t a)).hom y) hxz'.symm).trans <|
      hc.symm.trans <|
      (congrArg (fun y : F.obj X => ef.hom y) (htrivX a x')).trans hxz'