The map attribute

Adding @[map] to a lemma named H of shape ∀ .., f = g, where f and g are morphisms in some category C, creates a new lemma named H_map of the form ∀ .. {D} (F : C ⥤ D), F.map f = F.map g and then applies simp only [Functor.map_comp, Functor.map_id].

The generated lemma orders morphism universes before object universes, with source universes before target universes in each group. Source parameters retain their names and relative order within each group. A parameter used for both objects and morphisms goes in the morphism group; parameters unrelated to category universes come last.

There is also a term elaborator map_of% t for use within proofs.

def Mathlib.Tactic.CategoryTheory.Map.mapCompSimp (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

simp only with Functor.map_comp and Functor.map_id on a single expression (used on each side via simpEq).

Equations

• Mathlib.Tactic.CategoryTheory.Map.mapCompSimp e = Lean.Meta.simpOnlyNames [`CategoryTheory.Functor.map_comp, `CategoryTheory.Functor.map_id] e

def Mathlib.Tactic.CategoryTheory.Map.mapExprHom (type : Q(Prop)) (e : Q(«$type»)) (uLev vLev : Lean.Level) : Lean.Elab.TermElabM Lean.Expr

Build the functor map lemma for e : f = g with target category levels uLev, vLev.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.CategoryTheory.Map.mapExpr (pf : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Given a proof pf of ∀ .., f = g with f g morphisms in a category, produce a proof of the map lemma, quantifying over every target category D and every functor F : C ⥤ D. The target category uses fresh universe metavariables, which the attribute generalizes to parameters and map_of% leaves for the surrounding elaboration to determine.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.CategoryTheory.Map.mapStx : Lean.ParserDescr

Adding @[map] to a lemma named H of shape ∀ .., f = g, where f and g are morphisms in some category C, creates a new lemma named H_map of the form ∀ .. {D} (F : C ⥤ D), F.map f = F.map g and then applies simp only [Functor.map_comp, Functor.map_id].

Use @[map (attr := simp)] to mark both the original lemma and H_map as simp lemmas, and @[map (attr := reassoc)] to generate reassociated versions of both the original lemma and the _map lemma (@[reassoc (attr := map)] generates _map versions of both the original and the reassociated lemma, but this is of course less general than @[map (attr := reassoc)]). All four lemmas can be registered as simp lemmas with @[map (attr := reassoc (attr := simp))].

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.CategoryTheory.Map.«termMap_of%_» : Lean.ParserDescr

map_of% t, where t is an equality f = g between morphisms (possibly under ∀ binders), produces the corresponding statement with a functor applied and simp only [Functor.map_comp, Functor.map_id] on each side.

Equations

• One or more equations did not get rendered due to their size.