category_theory.endomorphism

def category_theory.End {C : Type u} [category_theory.category_struct C] (X : C) :

Type v

Endomorphisms of an object in a category. Arguments order in multiplication agrees with function.comp, not with category.comp.

Equations

category_theory.End X = (X ⟶ X)

source

@[protected, instance]

def category_theory.End.has_one {C : Type u} [category_theory.category_struct C] (X : C) :

has_one (category_theory.End X)

Equations

category_theory.End.has_one X = {one := 𝟙 X}

source

@[protected, instance]

def category_theory.End.inhabited {C : Type u} [category_theory.category_struct C] (X : C) :

inhabited (category_theory.End X)

Equations

category_theory.End.inhabited X = {default := 𝟙 X}

source

@[protected, instance]

def category_theory.End.has_mul {C : Type u} [category_theory.category_struct C] (X : C) :

has_mul (category_theory.End X)

Multiplication of endomorphisms agrees with function.comp, not category_struct.comp.

Equations

category_theory.End.has_mul X = {mul := λ (x y : category_theory.End X), y ≫ x}

source

def category_theory.End.of {C : Type u} [category_theory.category_struct C] {X : C} (f : X ⟶ X) :

category_theory.End X

Assist the typechecker by expressing a morphism X ⟶ X as a term of End X.

Equations

category_theory.End.of f = f

source

def category_theory.End.as_hom {C : Type u} [category_theory.category_struct C] {X : C} (f : category_theory.End X) :

X ⟶ X

Assist the typechecker by expressing an endomorphism f : End X as a term of X ⟶ X.

Equations

f.as_hom = f

source

@[simp]

theorem category_theory.End.one_def {C : Type u} [category_theory.category_struct C] {X : C} :

1 = 𝟙 X

source

@[simp]

theorem category_theory.End.mul_def {C : Type u} [category_theory.category_struct C] {X : C} (xs ys : category_theory.End X) :

xs * ys = ys ≫ xs

source

@[protected, instance]

def category_theory.End.monoid {C : Type u} [category_theory.category C] {X : C} :

monoid (category_theory.End X)

Endomorphisms of an object form a monoid

Equations

category_theory.End.monoid = {mul := has_mul.mul (category_theory.End.has_mul X), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (category_theory.End X)), npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def category_theory.End.mul_action_right {C : Type u} [category_theory.category C] {X Y : C} :

mul_action (category_theory.End Y) (X ⟶ Y)

Equations

category_theory.End.mul_action_right = {to_has_scalar := {smul := λ (r : category_theory.End Y) (f : X ⟶ Y), f ≫ r}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def category_theory.End.mul_action_left {C : Type u} [category_theory.category C] {X : Cᵒᵖ} {Y : C} :

mul_action (category_theory.End X) (opposite.unop X ⟶ Y)

Equations

category_theory.End.mul_action_left = {to_has_scalar := {smul := λ (r : category_theory.End X) (f : opposite.unop X ⟶ Y), quiver.hom.unop r ≫ f}, one_smul := _, mul_smul := _}

source

theorem category_theory.End.smul_right {C : Type u} [category_theory.category C] {X Y : C} {r : category_theory.End Y} {f : X ⟶ Y} :

r • f = f ≫ r

source

theorem category_theory.End.smul_left {C : Type u} [category_theory.category C] {X : Cᵒᵖ} {Y : C} {r : category_theory.End X} {f : opposite.unop X ⟶ Y} :

r • f = quiver.hom.unop r ≫ f

source

@[protected, instance]

def category_theory.End.group {C : Type u} [category_theory.groupoid C] (X : C) :

group (category_theory.End X)

In a groupoid, endomorphisms form a group

Equations

category_theory.End.group X = {mul := monoid.mul category_theory.End.monoid, mul_assoc := _, one := monoid.one category_theory.End.monoid, one_mul := _, mul_one := _, npow := monoid.npow category_theory.End.monoid, npow_zero' := _, npow_succ' := _, inv := category_theory.groupoid.inv X, div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ monoid.npow _ _ category_theory.groupoid.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul _ monoid.one _ _ monoid.npow _ _ category_theory.groupoid.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

theorem category_theory.is_unit_iff_is_iso {C : Type u} [category_theory.category C] {X : C} (f : category_theory.End X) :

is_unit f ↔ category_theory.is_iso f

source

def category_theory.Aut {C : Type u} [category_theory.category C] (X : C) :

Type v

Automorphisms of an object in a category.

The order of arguments in multiplication agrees with function.comp, not with category.comp.

Equations

category_theory.Aut X = (X ≅ X)

source

@[protected, instance]

def category_theory.Aut.inhabited {C : Type u} [category_theory.category C] (X : C) :

inhabited (category_theory.Aut X)

Equations

category_theory.Aut.inhabited X = {default := category_theory.iso.refl X}

source

@[protected, instance]

def category_theory.Aut.group {C : Type u} [category_theory.category C] (X : C) :

group (category_theory.Aut X)

Equations

category_theory.Aut.group X = {mul := flip category_theory.iso.trans, mul_assoc := _, one := category_theory.iso.refl X, one_mul := _, mul_one := _, npow := npow_rec {mul := flip category_theory.iso.trans}, npow_zero' := _, npow_succ' := _, inv := category_theory.iso.symm X, div := λ (a b : X ≅ X), a * b.symm, div_eq_mul_inv := _, zpow := zpow_rec {inv := category_theory.iso.symm X}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

theorem category_theory.Aut.Aut_mul_def {C : Type u} [category_theory.category C] (X : C) (f g : category_theory.Aut X) :

f * g = g ≪≫ f

source

def category_theory.Aut.units_End_equiv_Aut {C : Type u} [category_theory.category C] (X : C) :

(category_theory.End X)ˣ ≃* category_theory.Aut X

Units in the monoid of endomorphisms of an object are (multiplicatively) equivalent to automorphisms of that object.

Equations

category_theory.Aut.units_End_equiv_Aut X = {to_fun := λ (f : (category_theory.End X)ˣ), {hom := f.val, inv := f.inv, hom_inv_id' := _, inv_hom_id' := _}, inv_fun := λ (f : category_theory.Aut X), {val := f.hom, inv := f.inv, val_inv := _, inv_val := _}, left_inv := _, right_inv := _, map_mul' := _}

source

def category_theory.Aut.Aut_mul_equiv_of_iso {C : Type u} [category_theory.category C] {X Y : C} (h : X ≅ Y) :

category_theory.Aut X ≃* category_theory.Aut Y

Isomorphisms induce isomorphisms of the automorphism group

Equations

category_theory.Aut.Aut_mul_equiv_of_iso h = {to_fun := λ (x : category_theory.Aut X), {hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom, hom_inv_id' := _, inv_hom_id' := _}, inv_fun := λ (y : category_theory.Aut Y), {hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv, hom_inv_id' := _, inv_hom_id' := _}, left_inv := _, right_inv := _, map_mul' := _}

source

def category_theory.functor.map_End {C : Type u} [category_theory.category C] (X : C) {D : Type u'} [category_theory.category D] (f : C ⥤ D) :

category_theory.End X →* category_theory.End (f.obj X)

f.map as a monoid hom between endomorphism monoids.

Equations

category_theory.functor.map_End X f = {to_fun := f.map X, map_one' := _, map_mul' := _}

source

@[simp]

theorem category_theory.functor.map_End_apply {C : Type u} [category_theory.category C] (X : C) {D : Type u'} [category_theory.category D] (f : C ⥤ D) (ᾰ : X ⟶ X) :

⇑(category_theory.functor.map_End X f) ᾰ = f.map ᾰ

source

def category_theory.functor.map_Aut {C : Type u} [category_theory.category C] (X : C) {D : Type u'} [category_theory.category D] (f : C ⥤ D) :

category_theory.Aut X →* category_theory.Aut (f.obj X)

f.map_iso as a group hom between automorphism groups.

Equations

category_theory.functor.map_Aut X f = {to_fun := f.map_iso X, map_one' := _, map_mul' := _}

mathlib documentation

Endomorphisms #