## Stream: new members

### Topic: Turning bundled homomorphism equalities into pointwise ones

#### 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:

/-
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.abelian.basic
import category_theory.abelian.exact

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]

{hom_group := λ F G,
{ add := λ α β,
{ app := λ X,
{ to_fun := λ g, α.app X g + β.app X g,
map_zero' := by simp,
intros x y,
simp,
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
},
zero := _,
neg := _,
},

end category_theory.abelian


#### 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

#### Johan Commelin (Mar 15 2021 at 04:53):

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


#### Johan Commelin (Mar 15 2021 at 04:53):

and then rewrite with alpha.naturality

#### 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:

/-
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.abelian.basic
import category_theory.abelian.exact

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,
intros x y,
simp,
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,
intros g₁ g₂,
simp,
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
ext,
simp
end

{ hom_group := λ F G,
intros α β γ,
ext X g,
simp,
end,
zero := nat_zero C,
intros α,
ext X g,
change (nat_add C (nat_zero C) α).app X g = α.app X g,
simp,
unfold nat_zero,
simp,
end,
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,
intros α,
ext X g,
change (nat_add C (nat_neg C α) α).app X g = 0,
simp,
unfold nat_neg,
simp
end,
intros α β,
ext X g,
change (nat_add C α β).app X g = (nat_add C β α).app X g,
simp,
end
},
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,
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 (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.

#### Scott Morrison (Mar 16 2021 at 01:14):

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

#### 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.

#### Reed Mullanix (Mar 16 2021 at 01:15):

Maybe something about concrete categories could work?

#### 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. :-)

#### 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

#### Scott Morrison (Mar 16 2021 at 01:28):

Here is a bit of a simplification up to nat_add:

/-
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.abelian.basic
import category_theory.abelian.exact

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) :=

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,
intros x y,
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,
intros g₁ g₂,
simp,
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
ext,
simp
end

{ hom_group := λ F G,
intros α β γ,
ext X g,
simp,
end,
zero := nat_zero C,
intros α,
ext X g,
change (nat_add C (nat_zero C) α).app X g = α.app X g,
simp,
unfold nat_zero,
simp,
end,
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,
intros α,
ext X g,
change (nat_add C (nat_neg C α) α).app X g = 0,
simp,
unfold nat_neg,
simp
end,
intros α β,
ext X g,
change (nat_add C α β).app X g = (nat_add C β α).app X g,
simp,
end
},
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,
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 (Mar 16 2021 at 01:30):

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

#### Scott Morrison (Mar 16 2021 at 01:31):

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

#### Scott Morrison (Mar 16 2021 at 01:31):

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

#### Scott Morrison (Mar 16 2021 at 01:31):

Everything will be infinitely easier. :-)

#### 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.

#### 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