Opposite

📁 Source: Mathlib/CategoryTheory/Localization/Opposite.lean

Statistics

Metric	Count
Definitions op	1
Theorems op, op_iff, unop, op_iff, isLocalization_op, isoOfHom_op_inv, isoOfHom_unop	7
Total	8

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_iff 📖	mathematical	—	IsLocalization Opposite CategoryTheory.Category.opposite op CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	IsLocalization.op_iff

CategoryTheory.Functor.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	—	CategoryTheory.Functor.IsLocalization Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	of_equivalence_target CategoryTheory.Localization.isLocalization_op
op_iff 📖	mathematical	—	CategoryTheory.Functor.IsLocalization Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	unop op
unop 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.Functor.unop CategoryTheory.MorphismProperty.unop CategoryTheory.Category.toCategoryStruct	—	of_equivalences op CategoryTheory.MorphismProperty.le_isoClosure CategoryTheory.Localization.inverts CategoryTheory.isIso_unop

CategoryTheory.Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_op 📖	mathematical	—	CategoryTheory.Functor.IsLocalization Opposite CategoryTheory.MorphismProperty.Localization CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.instCategoryLocalization CategoryTheory.Functor.op CategoryTheory.MorphismProperty.Q CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Functor.IsLocalization.mk'
isoOfHom_op_inv 📖	mathematical	CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.inv Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.op isoOfHom CategoryTheory.Functor.IsLocalization.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.unop Quiver.Hom.unop	—	inverts CategoryTheory.Functor.IsLocalization.op isoOfHom_unop
isoOfHom_unop 📖	mathematical	CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op isoOfHom CategoryTheory.Functor.IsLocalization.op Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Iso.ext CategoryTheory.Functor.IsLocalization.op

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

Definitions

Name	Category	Theorems
op 📖	CompOp	—

---

← Back to Index