Mathlib Map

Structures · Category theory

CategoryTheory.Functor.ReflectsIsomorphisms

Define what it means for a functor F : C ⥤ D to reflect isomorphisms: for any morphism f : A ⟶ B, if F.map f is an isomorphism then f is as well. Note that we do not assume or require that F is faithful.

Defined in
Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
Shape
One type argument · adds reflects
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances62

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • ModuleCat
  • HomologicalComplex
  • CategoryTheory.Mon
  • AddCommGrpCat
  • Rep
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • SheafOfModules
  • CommRingCat
  • AlgebraicGeometry.LocallyRingedSpace
  • CategoryTheory.Under
  • CategoryTheory.Sheaf
  • AlgebraicGeometry.Scheme.Modules
  • CategoryTheory.CostructuredArrow
  • AlgCat
  • CategoryTheory.StructuredArrow
  • CommMonCat
  • ProfiniteGrp
  • CategoryTheory.Center
  • CategoryTheory.Limits.Cocone
  • CategoryTheory.Limits.Cone
  • AddCommMonCat
  • CategoryTheory.AddMon
  • CategoryTheory.MorphismProperty.Comma
  • MonCat
  • AddMonCat
  • CategoryTheory.Comonad.Coalgebra
  • CompHausLike
  • CategoryTheory.Monad.Algebra
  • SemimoduleCat
  • TopModuleCat
  • CommAlgCat
  • PartOrdEmb
  • RingCat
  • CommSemiRingCat
  • HopfAlgCat
  • CategoryTheory.Monad
  • CategoryTheory.Comon
  • CategoryTheory.Comonad
  • BialgCat
  • CategoryTheory.Idempotents.Karoubi
  • AddSemigrp
  • Semigrp
  • SemiRingCat
  • CoalgCat
  • CommBialgCat
  • TopCommRingCat
  • CommHopfAlgCat
  • AddMagmaCat
  • ProfiniteAddGrp
  • CategoryTheory.Endofunctor.Coalgebra
  • CategoryTheory.Endofunctor.Algebra
  • MagmaCat
  • CategoryTheory.Functor.Elements
  • CategoryTheory.BasedFunctor
  • LightProfinite
  • CategoryTheory.SimplicialObject
  • SimplexCategory
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by143

Ancestors0

No ancestors.