Category of Families as a Symmetric Monoidal Category

For any category C, the category Fam C of families forms a symmetric monoidal category with Sum as tensor and Empty as unit.

Objects are pairs (ι : Type, objs : ι → C). Morphisms carry an equivalence σ : ι₁ ≃ ι₂ together with componentwise C-morphisms.

The tensor uses Sum on index types and Sum.elim on objects, giving definitional reductions for all structural morphisms (associator, braiding, unitors).

Main results

• Category (FamObj C) — componentwise category with Equiv permutations
• MonoidalCategory (FamObj C) — Sum tensor, Empty unit
• BraidedCategory (FamObj C) — braiding via Sum.swap
• SymmetricCategory (FamObj C) — braiding is self-inverse

structure CatCrypt.Category.FamObj (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max 1 u)

Objects of the family category: a type ι indexing objects of C.

• ι : Type
• objs : self.ι → C

structure CatCrypt.Category.FamObj.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : Type v

Morphisms in the family category: an equivalence on index types with componentwise C-morphisms.

• σ : X.ι ≃ Y.ι
• map (i : X.ι) : X.objs i ⟶ Y.objs (self.σ i)

theorem CatCrypt.Category.FamObj.fam_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : FamObj C} {f g : X.Hom Y} (hσ : f.σ = g.σ) (hmap : ∀ (i : X.ι), f.map i ≍ g.map i) : f = g

Two morphisms are equal iff σ agrees and map agrees (up to HEq).

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instCategoryStruct {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.CategoryStruct.{v, max 1 u} (FamObj C)

Equations

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

@[simp]

theorem CatCrypt.Category.FamObj.comp_σ {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : FamObj C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).σ = f.σ.trans g.σ

@[simp]

theorem CatCrypt.Category.FamObj.comp_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : FamObj C} (f : X ⟶ Y) (g : Y ⟶ Z) (i : X.ι) : (CategoryTheory.CategoryStruct.comp f g).map i = CategoryTheory.CategoryStruct.comp (f.map i) (g.map (f.σ i))

@[simp]

theorem CatCrypt.Category.FamObj.id_σ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : (CategoryTheory.CategoryStruct.id X).σ = Equiv.refl X.ι

@[simp]

theorem CatCrypt.Category.FamObj.id_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) (i : X.ι) : (CategoryTheory.CategoryStruct.id X).map i = CategoryTheory.CategoryStruct.id (X.objs i)

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instCategory {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max 1 u} (FamObj C)

Equations

• CatCrypt.Category.FamObj.instCategory = { toCategoryStruct := CatCrypt.Category.FamObj.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

Monoidal definitions

def CatCrypt.Category.FamObj.tensorObj {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : FamObj C

Tensor product of families: Sum on index types, Sum.elim on objects.

Equations

• X.tensorObj Y = { ι := X.ι ⊕ Y.ι, objs := Sum.elim X.objs Y.objs }

def CatCrypt.Category.FamObj.unitObj {C : Type u} [CategoryTheory.Category.{v, u} C] : FamObj C

Unit for tensor: empty family.

Equations

• CatCrypt.Category.FamObj.unitObj = { ι := Empty, objs := Empty.elim }

noncomputable def CatCrypt.Category.FamObj.wkL {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (f : Y₁ ⟶ Y₂) : X.tensorObj Y₁ ⟶ X.tensorObj Y₂

Left whiskering: identity on the left component, f on the right.

Equations

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

noncomputable def CatCrypt.Category.FamObj.wkR {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) : X₁.tensorObj Y ⟶ X₂.tensorObj Y

Right whiskering: f on the left component, identity on the right.

Equations

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

noncomputable def CatCrypt.Category.FamObj.assocHom {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (X.tensorObj Y).tensorObj Z ⟶ X.tensorObj (Y.tensorObj Z)

Associator forward.

Equations

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

noncomputable def CatCrypt.Category.FamObj.assocInv {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : X.tensorObj (Y.tensorObj Z) ⟶ (X.tensorObj Y).tensorObj Z

Associator backward.

Equations

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

noncomputable def CatCrypt.Category.FamObj.braidHom {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : X.tensorObj Y ⟶ Y.tensorObj X

Braiding.

Equations

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

Left and right unitors

noncomputable def CatCrypt.Category.FamObj.lUnit {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : unitObj.tensorObj X ≅ X

Equations

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

noncomputable def CatCrypt.Category.FamObj.rUnit {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : X.tensorObj unitObj ≅ X

Equations

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

Equiv application lemmas

Mathlib's Equiv.sumCongr_apply doesn't fire in simp through the FunLike.coe discrimination tree. These specific lemmas bypass the issue by stating applications directly. All proved by rfl (definitional).

@[simp]

theorem CatCrypt.Category.FamObj.sumCongr_refl_inl {α α' β : Type} (e : α ≃ α') (a : α) : (e.sumCongr (Equiv.refl β)) (Sum.inl a) = Sum.inl (e a)

@[simp]

theorem CatCrypt.Category.FamObj.sumCongr_refl_inr {α α' β : Type} (e : α ≃ α') (b : β) : (e.sumCongr (Equiv.refl β)) (Sum.inr b) = Sum.inr b

@[simp]

theorem CatCrypt.Category.FamObj.refl_sumCongr_inl {α β β' : Type} (e : β ≃ β') (a : α) : ((Equiv.refl α).sumCongr e) (Sum.inl a) = Sum.inl a

@[simp]

theorem CatCrypt.Category.FamObj.refl_sumCongr_inr {α β β' : Type} (e : β ≃ β') (b : β) : ((Equiv.refl α).sumCongr e) (Sum.inr b) = Sum.inr (e b)

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_inl_inl {α β γ : Type} (a : α) : (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_inl_inr {α β γ : Type} (b : β) : (Equiv.sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_inr {α β γ : Type} (c : γ) : (Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_symm_inl {α β γ : Type} (a : α) : (Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_symm_inr_inl {α β γ : Type} (b : β) : (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)

@[simp]

theorem CatCrypt.Category.FamObj.sumAssoc_symm_inr_inr {α β γ : Type} (c : γ) : (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c

@[simp]

theorem CatCrypt.Category.FamObj.sumComm_inl {α β : Type} (a : α) : (Equiv.sumComm α β) (Sum.inl a) = Sum.inr a

@[simp]

theorem CatCrypt.Category.FamObj.sumComm_inr {α β : Type} (b : β) : (Equiv.sumComm α β) (Sum.inr b) = Sum.inl b

@[simp]

theorem CatCrypt.Category.FamObj.emptySum_inr {α : Type} (a : α) : (Equiv.emptySum Empty α) (Sum.inr a) = a

@[simp]

theorem CatCrypt.Category.FamObj.emptySum_symm_apply {α : Type} (a : α) : (Equiv.emptySum Empty α).symm a = Sum.inr a

@[simp]

theorem CatCrypt.Category.FamObj.sumEmpty_inl {α : Type} (a : α) : (Equiv.sumEmpty α Empty) (Sum.inl a) = a

@[simp]

theorem CatCrypt.Category.FamObj.sumEmpty_symm_apply {α : Type} (a : α) : (Equiv.sumEmpty α Empty).symm a = Sum.inl a

@[simp]

theorem CatCrypt.Category.FamObj.trans_apply' {α β γ : Type} (e₁ : α ≃ β) (e₂ : β ≃ γ) (a : α) : (e₁.trans e₂) a = e₂ (e₁ a)

Equiv-level σ lemmas

These rewrite Hom.σ (a struct projection returning an Equiv) to the concrete Equiv constructor. Since Hom.σ is a struct projection (not going through FunLike.coe), these fire reliably in simp.

@[simp]

theorem CatCrypt.Category.FamObj.wkL_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (f : Y₁ ⟶ Y₂) : (X.wkL f).σ = (Equiv.refl X.ι).sumCongr f.σ

@[simp]

theorem CatCrypt.Category.FamObj.wkR_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) : (wkR f Y).σ = f.σ.sumCongr (Equiv.refl Y.ι)

@[simp]

theorem CatCrypt.Category.FamObj.assocHom_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (X.assocHom Y Z).σ = Equiv.sumAssoc X.ι Y.ι Z.ι

@[simp]

theorem CatCrypt.Category.FamObj.assocInv_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (X.assocInv Y Z).σ = (Equiv.sumAssoc X.ι Y.ι Z.ι).symm

@[simp]

theorem CatCrypt.Category.FamObj.braidHom_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : (X.braidHom Y).σ = Equiv.sumComm X.ι Y.ι

@[simp]

theorem CatCrypt.Category.FamObj.lUnit_hom_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : X.lUnit.hom.σ = Equiv.emptySum Empty X.ι

@[simp]

theorem CatCrypt.Category.FamObj.lUnit_inv_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : X.lUnit.inv.σ = (Equiv.emptySum Empty X.ι).symm

@[simp]

theorem CatCrypt.Category.FamObj.rUnit_hom_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : X.rUnit.hom.σ = Equiv.sumEmpty X.ι Empty

@[simp]

theorem CatCrypt.Category.FamObj.rUnit_inv_σ_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : X.rUnit.inv.σ = (Equiv.sumEmpty X.ι Empty).symm

Per-constructor simp lemmas for map

These fire fine in simp because Hom.map is a direct struct projection (no FunLike.coe coercion chain).

@[simp]

theorem CatCrypt.Category.FamObj.wkL_map_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (f : Y₁ ⟶ Y₂) (a : X.ι) : (X.wkL f).map (Sum.inl a) = CategoryTheory.CategoryStruct.id ((X.tensorObj Y₁).objs (Sum.inl a))

@[simp]

theorem CatCrypt.Category.FamObj.wkL_map_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (f : Y₁ ⟶ Y₂) (b : Y₁.ι) : (X.wkL f).map (Sum.inr b) = f.map b

@[simp]

theorem CatCrypt.Category.FamObj.wkR_map_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) (a : X₁.ι) : (wkR f Y).map (Sum.inl a) = f.map a

@[simp]

theorem CatCrypt.Category.FamObj.wkR_map_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) (b : Y.ι) : (wkR f Y).map (Sum.inr b) = CategoryTheory.CategoryStruct.id ((X₁.tensorObj Y).objs (Sum.inr b))

@[simp]

theorem CatCrypt.Category.FamObj.assocHom_map_inl_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (a : X.ι) : (X.assocHom Y Z).map (Sum.inl (Sum.inl a)) = CategoryTheory.CategoryStruct.id (((X.tensorObj Y).tensorObj Z).objs (Sum.inl (Sum.inl a)))

@[simp]

theorem CatCrypt.Category.FamObj.assocHom_map_inl_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (b : Y.ι) : (X.assocHom Y Z).map (Sum.inl (Sum.inr b)) = CategoryTheory.CategoryStruct.id (((X.tensorObj Y).tensorObj Z).objs (Sum.inl (Sum.inr b)))

@[simp]

theorem CatCrypt.Category.FamObj.assocHom_map_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (c : Z.ι) : (X.assocHom Y Z).map (Sum.inr c) = CategoryTheory.CategoryStruct.id (((X.tensorObj Y).tensorObj Z).objs (Sum.inr c))

@[simp]

theorem CatCrypt.Category.FamObj.assocInv_map_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (a : X.ι) : (X.assocInv Y Z).map (Sum.inl a) = CategoryTheory.CategoryStruct.id ((X.tensorObj (Y.tensorObj Z)).objs (Sum.inl a))

@[simp]

theorem CatCrypt.Category.FamObj.assocInv_map_inr_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (b : Y.ι) : (X.assocInv Y Z).map (Sum.inr (Sum.inl b)) = CategoryTheory.CategoryStruct.id ((X.tensorObj (Y.tensorObj Z)).objs (Sum.inr (Sum.inl b)))

@[simp]

theorem CatCrypt.Category.FamObj.assocInv_map_inr_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) (c : Z.ι) : (X.assocInv Y Z).map (Sum.inr (Sum.inr c)) = CategoryTheory.CategoryStruct.id ((X.tensorObj (Y.tensorObj Z)).objs (Sum.inr (Sum.inr c)))

@[simp]

theorem CatCrypt.Category.FamObj.braidHom_map_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) (a : X.ι) : (X.braidHom Y).map (Sum.inl a) = CategoryTheory.CategoryStruct.id ((X.tensorObj Y).objs (Sum.inl a))

@[simp]

theorem CatCrypt.Category.FamObj.braidHom_map_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) (b : Y.ι) : (X.braidHom Y).map (Sum.inr b) = CategoryTheory.CategoryStruct.id ((X.tensorObj Y).objs (Sum.inr b))

@[simp]

theorem CatCrypt.Category.FamObj.lUnit_hom_map_inr {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) (a : X.ι) : X.lUnit.hom.map (Sum.inr a) = CategoryTheory.CategoryStruct.id ((unitObj.tensorObj X).objs (Sum.inr a))

@[simp]

theorem CatCrypt.Category.FamObj.lUnit_inv_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) (a : X.ι) : X.lUnit.inv.map a = CategoryTheory.CategoryStruct.id (X.objs a)

@[simp]

theorem CatCrypt.Category.FamObj.rUnit_hom_map_inl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) (a : X.ι) : X.rUnit.hom.map (Sum.inl a) = CategoryTheory.CategoryStruct.id ((X.tensorObj unitObj).objs (Sum.inl a))

@[simp]

theorem CatCrypt.Category.FamObj.rUnit_inv_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) (a : X.ι) : X.rUnit.inv.map a = CategoryTheory.CategoryStruct.id (X.objs a)

Small morphism-level lemmas

These operate at the level of whole morphisms (not components), allowing MonoidalCategory axioms to be proved by rewriting rather than fam_ext.

@[simp]

theorem CatCrypt.Category.FamObj.wkL_id {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : X.wkL (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X.tensorObj Y)

@[simp]

theorem CatCrypt.Category.FamObj.wkR_id {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : wkR (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (X.tensorObj Y)

@[simp]

theorem CatCrypt.Category.FamObj.wkL_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ Y₃ : FamObj C} (f : Y₁ ⟶ Y₂) (g : Y₂ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (X.wkL f) (X.wkL g) = X.wkL (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CatCrypt.Category.FamObj.wkL_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ Y₃ : FamObj C} (f : Y₁ ⟶ Y₂) (g : Y₂ ⟶ Y₃) {Z : FamObj C} (h : X.tensorObj Y₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.wkL f) (CategoryTheory.CategoryStruct.comp (X.wkL g) h) = CategoryTheory.CategoryStruct.comp (X.wkL (CategoryTheory.CategoryStruct.comp f g)) h

@[simp]

theorem CatCrypt.Category.FamObj.wkR_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ : FamObj C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (Y : FamObj C) : CategoryTheory.CategoryStruct.comp (wkR f Y) (wkR g Y) = wkR (CategoryTheory.CategoryStruct.comp f g) Y

@[simp]

theorem CatCrypt.Category.FamObj.wkR_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ : FamObj C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (Y : FamObj C) {Z : FamObj C} (h : X₃.tensorObj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (wkR f Y) (CategoryTheory.CategoryStruct.comp (wkR g Y) h) = CategoryTheory.CategoryStruct.comp (wkR (CategoryTheory.CategoryStruct.comp f g) Y) h

@[simp]

theorem CatCrypt.Category.FamObj.wkR_wkL_comm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : FamObj C} (g : Y₁ ⟶ Y₂) : CategoryTheory.CategoryStruct.comp (wkR f Y₁) (X₂.wkL g) = CategoryTheory.CategoryStruct.comp (X₁.wkL g) (wkR f Y₂)

@[simp]

theorem CatCrypt.Category.FamObj.wkR_wkL_comm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : FamObj C} (g : Y₁ ⟶ Y₂) {Z : FamObj C} (h : X₂.tensorObj Y₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (wkR f Y₁) (CategoryTheory.CategoryStruct.comp (X₂.wkL g) h) = CategoryTheory.CategoryStruct.comp (X₁.wkL g) (CategoryTheory.CategoryStruct.comp (wkR f Y₂) h)

Naturality lemmas for structural morphisms

These express naturality of assocHom, braidHom, and unitors with respect to wkR/wkL. Proofs use erw which matches through dependent function arguments via isDefEq, unlike simp/dsimp which use discrimination trees.

theorem CatCrypt.Category.FamObj.assocHom_wkR {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y Z : FamObj C) : CategoryTheory.CategoryStruct.comp (wkR (wkR f Y) Z) (X₂.assocHom Y Z) = CategoryTheory.CategoryStruct.comp (X₁.assocHom Y Z) (wkR f (Y.tensorObj Z))

theorem CatCrypt.Category.FamObj.assocHom_wkL_mid {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (g : Y₁ ⟶ Y₂) (Z : FamObj C) : CategoryTheory.CategoryStruct.comp (wkR (X.wkL g) Z) (X.assocHom Y₂ Z) = CategoryTheory.CategoryStruct.comp (X.assocHom Y₁ Z) (X.wkL (wkR g Z))

theorem CatCrypt.Category.FamObj.assocHom_wkL_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) {Z₁ Z₂ : FamObj C} (h : Z₁ ⟶ Z₂) : CategoryTheory.CategoryStruct.comp ((X.tensorObj Y).wkL h) (X.assocHom Y Z₂) = CategoryTheory.CategoryStruct.comp (X.assocHom Y Z₁) (X.wkL (Y.wkL h))

theorem CatCrypt.Category.FamObj.braidHom_wkR {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) : CategoryTheory.CategoryStruct.comp (wkR f Y) (X₂.braidHom Y) = CategoryTheory.CategoryStruct.comp (X₁.braidHom Y) (Y.wkL f)

theorem CatCrypt.Category.FamObj.braidHom_wkL {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (g : Y₁ ⟶ Y₂) : CategoryTheory.CategoryStruct.comp (X.wkL g) (X.braidHom Y₂) = CategoryTheory.CategoryStruct.comp (X.braidHom Y₁) (wkR g X)

Isomorphisms

noncomputable def CatCrypt.Category.FamObj.assocIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (X.tensorObj Y).tensorObj Z ≅ X.tensorObj (Y.tensorObj Z)

Equations

• X.assocIso Y Z = { hom := X.assocHom Y Z, inv := X.assocInv Y Z, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CatCrypt.Category.FamObj.braidIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : X.tensorObj Y ≅ Y.tensorObj X

Equations

• X.braidIso Y = { hom := X.braidHom Y, inv := Y.braidHom X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem CatCrypt.Category.FamObj.braidIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : (X.braidIso Y).hom = X.braidHom Y

theorem CatCrypt.Category.FamObj.braidIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : FamObj C) : (X.braidIso Y).inv = Y.braidHom X

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instMonoidalCategoryStruct {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.MonoidalCategoryStruct (FamObj C)

Equations

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

Simp lemmas bridging class projections to concrete definitions

@[simp]

theorem CatCrypt.Category.FamObj.whiskerLeft_def {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) {Y₁ Y₂ : FamObj C} (f : Y₁ ⟶ Y₂) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = X.wkL f

@[simp]

theorem CatCrypt.Category.FamObj.whiskerRight_def {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ : FamObj C} (f : X₁ ⟶ X₂) (Y : FamObj C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = wkR f Y

@[simp]

theorem CatCrypt.Category.FamObj.tensorHom_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ Y₁ X₂ Y₂ : FamObj C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.CategoryStruct.comp (wkR f X₂) (Y₁.wkL g)

@[simp]

theorem CatCrypt.Category.FamObj.associator_hom_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = X.assocHom Y Z

@[simp]

theorem CatCrypt.Category.FamObj.associator_inv_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y Z : FamObj C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = X.assocInv Y Z

@[simp]

theorem CatCrypt.Category.FamObj.leftUnitor_hom_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = X.lUnit.hom

@[simp]

theorem CatCrypt.Category.FamObj.rightUnitor_hom_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (X : FamObj C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = X.rUnit.hom

Tactic for map-field goals

For goals involving only structural morphisms (all 𝟙 map components), erw with isDefEq matching can rewrite inside dependent function arguments where simp/dsimp discrimination trees cannot. The pattern is:

1. erw [FamObj.comp_map] to expand compositions
2. erw [specific_map_lemma] to reduce individual .map calls
3. erw [Category.id_comp] to close residual 𝟙 ≫ 𝟙 = 𝟙 goals

For naturality axioms, we use morphism-level intermediate lemmas (assocHom_wkR, braidHom_wkR, etc.) to avoid complex erw chains.

MonoidalCategory

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instMonoidalCategory {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.MonoidalCategory (FamObj C)

Equations

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

BraidedCategory and SymmetricCategory

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instBraidedCategory {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.BraidedCategory (FamObj C)

Equations

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

@[implicit_reducible]

noncomputable instance CatCrypt.Category.FamObj.instSymmetricCategory {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.SymmetricCategory (FamObj C)

Equations

• CatCrypt.Category.FamObj.instSymmetricCategory = { toBraidedCategory := CatCrypt.Category.FamObj.instBraidedCategory, symmetry := ⋯ }