Automorphisms in a category

This file contains general bookkeeping lemmas for automorphisms of objects in a category.

Main results

• TauCeti.CategoryTheory.comp_aut_pow_hom_of_comp: iterating an automorphism that reindexes a family of morphisms reindexes that family by the corresponding function iterate.
• TauCeti.CategoryTheory.autMulEquivOfIso_hom: the forward component of an automorphism transported along an isomorphism.

@[simp]

theorem TauCeti.CategoryTheory.autMulEquivOfIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : X ≅ Y) (a : CategoryTheory.Aut X) : ((CategoryTheory.Aut.autMulEquivOfIso h) a).hom = CategoryTheory.CategoryStruct.comp h.inv (CategoryTheory.CategoryStruct.comp a.hom h.hom)

The forward component of an automorphism transported along an isomorphism is the conjugate of its forward component. Aut.autMulEquivOfIso is not equipped with @[simps], so this is the characterization its consumers use instead of its constructor.

theorem TauCeti.CategoryTheory.comp_aut_pow_hom_of_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {iota : Type u_1} (gamma : CategoryTheory.Aut X) (F : iota → (Y ⟶ X)) (s : iota → iota) (h : ∀ (i : iota), CategoryTheory.CategoryStruct.comp (F i) gamma.hom = F (s i)) (m : ℕ) (i : iota) : CategoryTheory.CategoryStruct.comp (F i) (gamma ^ m).hom = F (s^[m] i)

Iterating an automorphism which reindexes a family of morphisms reindexes that family by the corresponding function iterate.