Documentation

TauCeti.CategoryTheory.Aut.Representable

Automorphisms of a represented presheaf #

Let a presheaf F : Cᵒᵖ ⥤ Type w be represented by an object Y, through natural bijections homEquiv : (X ⟶ Y) ≃ F(X). By the Yoneda lemma, automorphisms of F are the same as automorphisms of Y: an automorphism σ of F corresponds to the unique automorphism s of Y with homEquiv (f ≫ s) = σ (homEquiv f) for every f : X ⟶ Y. This file records the correspondence as an isomorphism of groups Aut F ≃* Aut Y (CategoryTheory.Functor.RepresentableBy.autMulEquiv). Composing with it turns an action of a group on a represented presheaf into an action on the representing object.

The presheaf may take values in any universe w, unrelated to the universe v of morphisms of C. This is the generality of moduli problems, which take values in a larger universe than the morphisms of their category of test objects. Mathlib identifies a representation with an isomorphism to the Yoneda functor only when F takes values in Type v (CategoryTheory.Functor.RepresentableBy.toIso), or with an isomorphism to the lifted Yoneda functor when F takes values in Type (max w v) (CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso), where the universe w cannot be inferred from F and has to be given explicitly. The correspondence here needs neither: the automorphism of Y attached to σ compares the representation of F by Y with its transport along σ, by uniqueness of representing objects (CategoryTheory.Functor.RepresentableBy.uniqueUpToIso).

Main definitions #

Main results #

source
theorem CategoryTheory.Functor.RepresentableBy.homEquiv_uniqueUpToIso_hom {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) {Y' : C} (R' : F.RepresentableBy Y') :
R'.homEquiv (R.uniqueUpToIso R').hom = R.homEquiv (CategoryStruct.id Y)

The isomorphism between two representing objects of F classifies, under the second representation, the universal element of the first.

source
def CategoryTheory.Functor.RepresentableBy.autMulEquiv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) :
Aut F ≃* Aut Y

Automorphisms of a represented presheaf are automorphisms of the representing object. If F is represented by Y, an automorphism σ of F corresponds to the automorphism s of Y with homEquiv (f ≫ s) = σ (homEquiv f) for every f : X ⟶ Y (homEquiv_comp_autMulEquiv_hom); an automorphism s of Y corresponds to postcomposition with s (autMulEquiv_symm_hom_app).

Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.RepresentableBy.homEquiv_comp_autMulEquiv_hom {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) (σ : Aut F) {X : C} (f : X ⟶ Y) :
    R.homEquiv (CategoryStruct.comp f (R.autMulEquiv σ).asIso.hom) = (ConcreteCategory.hom (σ.asIso.hom.app (Opposite.op X))) (R.homEquiv f)

    The automorphism of Y attached to an automorphism σ of F acts on homEquiv f as σ.

    source
    @[simp]
    theorem CategoryTheory.Functor.RepresentableBy.homEquiv_comp_autMulEquiv_inv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) (σ : Aut F) {X : C} (f : X ⟶ Y) :
    R.homEquiv (CategoryStruct.comp f (R.autMulEquiv σ).asIso.inv) = (ConcreteCategory.hom (σ.asIso.inv.app (Opposite.op X))) (R.homEquiv f)

    The inverse of the automorphism of Y attached to an automorphism σ of F acts on homEquiv f as the inverse of σ.

    source
    @[simp]
    theorem CategoryTheory.Functor.RepresentableBy.homEquiv_autMulEquiv_hom {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) (σ : Aut F) :
    R.homEquiv (R.autMulEquiv σ).asIso.hom = (ConcreteCategory.hom (σ.asIso.hom.app (Opposite.op Y))) (R.homEquiv (CategoryStruct.id Y))

    The automorphism of Y attached to an automorphism σ of F classifies the image under σ of the universal element homEquiv (𝟙 Y).

    source
    @[simp]
    theorem CategoryTheory.Functor.RepresentableBy.homEquiv_autMulEquiv_inv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) (σ : Aut F) :
    R.homEquiv (R.autMulEquiv σ).asIso.inv = (ConcreteCategory.hom (σ.asIso.inv.app (Opposite.op Y))) (R.homEquiv (CategoryStruct.id Y))

    The inverse of the automorphism of Y attached to an automorphism σ of F classifies the image under σ⁻¹ of the universal element homEquiv (𝟙 Y).

    source
    @[simp]
    theorem CategoryTheory.Functor.RepresentableBy.autMulEquiv_symm_hom_app {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {Y : C} (R : F.RepresentableBy Y) (s : Aut Y) {X : C} (x : F.obj (Opposite.op X)) :
    (ConcreteCategory.hom ((R.autMulEquiv.symm s).asIso.hom.app (Opposite.op X))) x = R.homEquiv (CategoryStruct.comp (R.homEquiv.symm x) s.asIso.hom)

    The automorphism of F attached to an automorphism s of Y is postcomposition with s.

    source
    theorem TauCeti.homEquiv_ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} {Y X : C} {R : F.RepresentableBy Y} {e : F ≅ G} {f : X ⟶ Y} :
    (R.ofIso e).homEquiv f = (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op X))) (R.homEquiv f)

    Transporting a representation along a presheaf isomorphism applies that isomorphism to its classifying element.