Theorems · Definition · category theory
CategoryTheory.Aut
{C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type vAutomorphisms of an object in a category.
The order of arguments in multiplication agrees with
Function.comp, not with CategoryTheory.CategoryStruct.comp.
- Defined in
- Mathlib.CategoryTheory.Endomorphism
- Cited by
- 96 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Isoproof · cited by 3,963
Cited by127
Results whose statement or proof uses this declaration.
- CategoryTheory.PreGaloisCategory.autMapstatement and proof · cited by 10
- CategoryTheory.PreGaloisCategory.toAutstatement · cited by 10
- CategoryTheory.PreGaloisCategory.AutGalois.πstatement · cited by 9
- CategoryTheory.PreGaloisCategory.functorToActionstatement and proof · cited by 8
- CategoryTheory.Iso.conjAutstatement · cited by 8
- CategoryTheory.PreGaloisCategory.autEmbeddingstatement and proof · cited by 6
- CategoryTheory.PreGaloisCategory.autGaloisSystemproof · cited by 6
- CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGaloisstatement and proof · cited by 6
- CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnectedstatement · cited by 6
- CategoryTheory.Aut.extstatement and proof · cited by 5
- CategoryTheory.PreGaloisCategory.autMulEquivAutGaloisstatement and proof · cited by 4
- CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithfulstatement and proof · cited by 4