Turning bundled homomorphism equalities into pointwise ones

Stream: new members

[Reed Mullanix]

I'm playing around with some stuff regarding abelian categories, and I'm getting stuck trying to turn a proof that two homs in CommAddGroup are equal into one that I can apply pointwise. More specifically, I have a proof F.F.map f ≫ α.app Y = α.app X ≫ G.F.map f in my hands, and I want to be able to turn this into something of the form that (α.app Y) ((F.F.map f) x) = (G.F.map f) ((α.app X) x). I've tried congr_fun, but it yells about some type mismatch with metavariables.

The code in question:

/-
Copyright (c) 2020 Reed Mullanix. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reed Mullanix
-/


import algebra.category.Group.basic
import algebra.category.Group.abelian

import category_theory.fin_category
import category_theory.full_subcategory
import category_theory.functor_category
import category_theory.limits.shapes.finite_limits

import category_theory.preadditive
import category_theory.abelian.basic
import category_theory.abelian.exact

open AddCommGroup

open category_theory
open category_theory.limits

namespace category_theory.abelian

universes v u₁ u₂

section
variables (C : Type u₁) [category.{v} C]
variables (D : Type u₂) [category.{v} D]

/-
First, let us start by defining left exact functors, and some simple properties
-/
structure left_exact_functor :=
(F : C ⥤ D)
(preserves_finite_limits : Π {J : Type v} [𝒥 : small_category J] [@fin_category J 𝒥], by exactI preserves_limits_of_shape J F)

instance left_exact_functors : category (left_exact_functor C D):=
induced_category.category left_exact_functor.F

end

variables (C : Type u₁) [category.{v} C]

instance : preadditive (left_exact_functor C AddCommGroup.{v}) :=
{hom_group := λ F G,
  { add := λ α β,
    { app := λ X,
      { to_fun := λ g, α.app X g + β.app X g,
        map_zero' := by simp,
        map_add' := begin
          intros x y,
          simp,
          exact add_add_add_comm (α.app X x) (α.app X y) (β.app X x) (β.app X y)
        end
      },
      naturality' := begin
        intros X Y f,
        ext,
        simp,
        -- Stuck right here! This is the proof that I want to make into a pointwise one.
        have α_nat := (α.naturality f),
        sorry
      end
    },
    add_assoc := _,
    zero := _,
    zero_add := _,
    add_zero := _,
    neg := _,
    add_left_neg := _,
    add_comm := _
  },
  add_comp' := _,
  comp_add' := _ }

end category_theory.abelian

[Johan Commelin]

I don't know if there are helper lemmas for this, but you can brute force your way through this by using change

[Johan Commelin]

change (a >> b) x = (c >> d) x,

[Johan Commelin]

and then rewrite with alpha.naturality

[Scott Morrison]

src#add_monoid_hom.congr_fun

[Reed Mullanix]

Managed to prove everything but there is a loooot of change magic involved to get things to compute nicely. Feels like I'm missing some obvious tool:

/-
Copyright (c) 2020 Reed Mullanix. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reed Mullanix
-/


import algebra.category.Group.basic
import algebra.category.Group.abelian

import category_theory.fin_category
import category_theory.full_subcategory
import category_theory.functor_category
import category_theory.limits.shapes.finite_limits

import category_theory.preadditive
import category_theory.abelian.basic
import category_theory.abelian.exact

open AddCommGroup

open category_theory
open category_theory.limits

namespace category_theory.abelian

universes v u₁ u₂

section
variables (C : Type u₁) [category.{v} C]
variables (D : Type u₂) [category.{v} D]

/-
First, let us start by defining left exact functors, and some simple properties
-/
structure left_exact_functor :=
(F : C ⥤ D)
(preserves_finite_limits : Π {J : Type v} [𝒥 : small_category J] [@fin_category J 𝒥], by exactI preserves_limits_of_shape J F)

instance left_exact_functors : category (left_exact_functor C D):=
induced_category.category left_exact_functor.F

def natural_transformation_add [preadditive D] {F G : C ⥤ D} (α β : F ⟶ G) : F ⟶ G :=
  { app := λ X, α.app X + β.app X }

end

variables (C : Type u₁) [category.{v} C]

def nat_add {F G : left_exact_functor C AddCommGroup.{v}} (α β : F ⟶ G) : F ⟶ G :=
  { app := λ X,
    { to_fun := λ g, α.app X g + β.app X g,
      map_zero' := by simp,
      map_add' := begin
        intros x y,
        simp,
        exact add_add_add_comm (α.app X x) (α.app X y) (β.app X x) (β.app X y)
      end
    },
    naturality' := begin
      intros X Y f,
      ext,
      simp,
      -- We have to do a bit of a silly dance here to get the naturality proofs to work pointwise.
      have α_nat : α.app Y (F.F.map f x) = G.F.map f (α.app X x) := add_monoid_hom.congr_fun (α.naturality f) x,
      have β_nat : β.app Y (F.F.map f x) = G.F.map f (β.app X x) := add_monoid_hom.congr_fun (β.naturality f) x,
      rw [α_nat, β_nat]
    end
  }

def nat_zero {F G : left_exact_functor C AddCommGroup.{v}} : F ⟶ G :=
  { app := λ _, 0,
  }

def nat_neg {F G : left_exact_functor C AddCommGroup.{v}} (α : F ⟶ G) : F ⟶ G :=
  { app := λ X,
    { to_fun := λ g, - (α.app X g),
      map_zero' := by simp,
      map_add' := begin
        intros g₁ g₂,
        simp,
        rw [add_comm _ _]
      end
    },
    naturality' := begin
      intros X Y f,
      ext x,
      simp,
      -- We have to do a bit of a silly dance here to get the naturality proofs to work pointwise.
      have α_nat : α.app Y (F.F.map f x) = G.F.map f (α.app X x) := add_monoid_hom.congr_fun (α.naturality f) x,
      exact α_nat
    end
  }

@[simp] lemma nat_add_homo {F G : left_exact_functor C AddCommGroup.{v}} (α β : F ⟶ G) (X : C) : (nat_add C α β).app X = (α.app X) + (β.app X) := begin
  unfold nat_add,
  ext,
  simp
end

instance : preadditive (left_exact_functor C AddCommGroup.{v}) :=
  { hom_group := λ F G,
    { add := nat_add C,
      add_assoc := begin
        intros α β γ,
        ext X g,
        simp,
        rw [add_assoc _ _ _]
      end,
      zero := nat_zero C,
      zero_add := begin
        intros α,
        ext X g,
        change (nat_add C (nat_zero C) α).app X g = α.app X g,
        simp,
        unfold nat_zero,
        simp,
      end,
      add_zero := begin
        intros α,
        ext X g,
        change (nat_add C α (nat_zero C)).app X g = α.app X g,
        simp,
        unfold nat_zero,
        simp
      end,
      neg := nat_neg C,
      add_left_neg := begin
        intros α,
        ext X g,
        change (nat_add C (nat_neg C α) α).app X g = 0,
        simp,
        unfold nat_neg,
        simp
      end,
      add_comm := begin
        intros α β,
        ext X g,
        change (nat_add C α β).app X g = (nat_add C β α).app X g,
        simp,
        rw [add_comm _ _]
      end
    },
    add_comp' := begin
      intros F G H α β γ,
      ext X g,
      -- Even more golf to get this to a place where simp can handle it
      change γ.app X ((nat_add C α β).app X g) = ((nat_add C (α ≫ γ) (β ≫ γ)).app X) g,
      simp,
      change γ.app X (α.app X g) + γ.app X (β.app X g) = γ.app X (α.app X g) + γ.app X (β.app X g),
      refl
    end,
    comp_add' := begin
      intros F G H α β γ,
      ext X g,
      change (nat_add C β γ).app X (α.app X g) = (nat_add C (α ≫ β) (α ≫ γ)).app X g,
      simp,
      change β.app X (α.app X g) + γ.app X (α.app X g) = β.app X (α.app X g) + γ.app X (α.app X g),
      refl
    end
  }

end category_theory.abelian

[Scott Morrison]

Likely we can add a lemma (even with @[simp]) for any category where the morphisms have a function coercion, for the "naturality applied at a point" statement. This may be less painful.

[Scott Morrison]

Hmm, maybe you can't make it that general.

[Reed Mullanix]

Seems reasonable to me, but I'm pretty inexperienced with exactly how/when lean decides to compute things down.

[Reed Mullanix]

Maybe something about concrete categories could work?

[Scott Morrison]

In any case, doing it generally is probably best punted until someone works out how to do enriched categories nicely. :-)

[Reed Mullanix]

Fair enough :smile: I am a bit confused as to why dsimp cant handle this, but I can keep throwing change around blindly so it isn't a blocker

[Scott Morrison]

Here is a bit of a simplification up to nat_add:

/-
Copyright (c) 2020 Reed Mullanix. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reed Mullanix
-/


import algebra.category.Group.basic
import algebra.category.Group.abelian

import category_theory.fin_category
import category_theory.full_subcategory
import category_theory.functor_category
import category_theory.limits.shapes.finite_limits

import category_theory.preadditive
import category_theory.abelian.basic
import category_theory.abelian.exact

open AddCommGroup

open category_theory
open category_theory.limits

universes v u₁ u₂

namespace category_theory.nat_trans

variables {C : Type u₁} [category.{v} C]

-- TODO generalize this to any concrete category?
@[simp]
lemma naturality_apply
  {F G : C ⥤ AddCommGroup} (α : F ⟶ G) ⦃X Y : C⦄ (f : X ⟶ Y) (x : F.obj X) :
  α.app Y (F.map f x) = G.map f (α.app X x) :=
add_monoid_hom.congr_fun (α.naturality f) x

end category_theory.nat_trans

open category_theory

namespace category_theory.abelian

section
variables (C : Type u₁) [category.{v} C]
variables (D : Type u₂) [category.{v} D]

/-
First, let us start by defining left exact functors, and some simple properties
-/
structure left_exact_functor :=
(F : C ⥤ D)
(preserves_finite_limits : Π {J : Type v} [𝒥 : small_category J] [@fin_category J 𝒥], by exactI preserves_limits_of_shape J F)

instance left_exact_functors : category (left_exact_functor C D):=
induced_category.category left_exact_functor.F

def natural_transformation_add [preadditive D] {F G : C ⥤ D} (α β : F ⟶ G) : F ⟶ G :=
  { app := λ X, α.app X + β.app X }

end

variables (C : Type u₁) [category.{v} C]

def nat_add {F G : left_exact_functor C AddCommGroup.{v}} (α β : F ⟶ G) : F ⟶ G :=
  { app := λ X,
    { to_fun := λ g, α.app X g + β.app X g,
      map_zero' := by simp,
      map_add' := begin
        intros x y,
        simp [add_add_add_comm],
      end
    },
    naturality' := begin
      intros X Y f,
      ext,
      simp,
    end
  }

def nat_zero {F G : left_exact_functor C AddCommGroup.{v}} : F ⟶ G :=
  { app := λ _, 0,
  }

def nat_neg {F G : left_exact_functor C AddCommGroup.{v}} (α : F ⟶ G) : F ⟶ G :=
  { app := λ X,
    { to_fun := λ g, - (α.app X g),
      map_zero' := by simp,
      map_add' := begin
        intros g₁ g₂,
        simp,
        rw [add_comm _ _]
      end
    },
    naturality' := begin
      intros X Y f,
      ext x,
      simp,
      -- We have to do a bit of a silly dance here to get the naturality proofs to work pointwise.
      have α_nat : α.app Y (F.F.map f x) = G.F.map f (α.app X x) := add_monoid_hom.congr_fun (α.naturality f) x,
      exact α_nat
    end
  }

@[simp] lemma nat_add_homo {F G : left_exact_functor C AddCommGroup.{v}} (α β : F ⟶ G) (X : C) : (nat_add C α β).app X = (α.app X) + (β.app X) := begin
  unfold nat_add,
  ext,
  simp
end

instance : preadditive (left_exact_functor C AddCommGroup.{v}) :=
  { hom_group := λ F G,
    { add := nat_add C,
      add_assoc := begin
        intros α β γ,
        ext X g,
        simp,
        rw [add_assoc _ _ _]
      end,
      zero := nat_zero C,
      zero_add := begin
        intros α,
        ext X g,
        change (nat_add C (nat_zero C) α).app X g = α.app X g,
        simp,
        unfold nat_zero,
        simp,
      end,
      add_zero := begin
        intros α,
        ext X g,
        change (nat_add C α (nat_zero C)).app X g = α.app X g,
        simp,
        unfold nat_zero,
        simp
      end,
      neg := nat_neg C,
      add_left_neg := begin
        intros α,
        ext X g,
        change (nat_add C (nat_neg C α) α).app X g = 0,
        simp,
        unfold nat_neg,
        simp
      end,
      add_comm := begin
        intros α β,
        ext X g,
        change (nat_add C α β).app X g = (nat_add C β α).app X g,
        simp,
        rw [add_comm _ _]
      end
    },
    add_comp' := begin
      intros F G H α β γ,
      ext X g,
      -- Even more golf to get this to a place where simp can handle it
      change γ.app X ((nat_add C α β).app X g) = ((nat_add C (α ≫ γ) (β ≫ γ)).app X) g,
      simp,
      change γ.app X (α.app X g) + γ.app X (β.app X g) = γ.app X (α.app X g) + γ.app X (β.app X g),
      refl
    end,
    comp_add' := begin
      intros F G H α β γ,
      ext X g,
      change (nat_add C β γ).app X (α.app X g) = (nat_add C (α ≫ β) (α ≫ γ)).app X g,
      simp,
      change β.app X (α.app X g) + γ.app X (α.app X g) = β.app X (α.app X g) + γ.app X (α.app X g),
      refl
    end
  }

end category_theory.abelian

[Scott Morrison]

I get a timeout on the last instance: you should break it into smaller pieces.

[Scott Morrison]

Ah, so the basic problem is that you are making defs without corresponding simp lemmas.

[Scott Morrison]

Just try sticking @[simps] on nat_add and nat_zero.

[Scott Morrison]

Everything will be infinitely easier. :-)

[Scott Morrison]

Anytime you find yourself using change or unfold, you should be thinking "how could I have got dsimp or simp to do this itself", and the answer is nearly always "write more @[simp] lemmas.

[Reed Mullanix]

Welp, adding @[simps] seems to be the magic ingredient I was missing! Breaking up the preadditive instance is a good call, bad habit of mine.