Zulip Chat Archive

Stream: new members

Topic: Turning bundled homomorphism equalities into pointwise ones


view this post on Zulip Reed Mullanix (Mar 15 2021 at 04:16):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 04:52):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 04:53):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 04:53):

and then rewrite with alpha.naturality

view this post on Zulip Scott Morrison (Mar 15 2021 at 06:50):

src#add_monoid_hom.congr_fun

view this post on Zulip Reed Mullanix (Mar 16 2021 at 01:00):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:11):

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.

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:14):

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

view this post on Zulip Reed Mullanix (Mar 16 2021 at 01:14):

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

view this post on Zulip Reed Mullanix (Mar 16 2021 at 01:15):

Maybe something about concrete categories could work?

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:15):

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

view this post on Zulip Reed Mullanix (Mar 16 2021 at 01:18):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:28):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:30):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:31):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:31):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:31):

Everything will be infinitely easier. :-)

view this post on Zulip Scott Morrison (Mar 16 2021 at 01:33):

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.

view this post on Zulip Reed Mullanix (Mar 16 2021 at 06:09):

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.


Last updated: May 06 2021 at 22:13 UTC