Theorems · Definition · category theory
CategoryTheory.MonoOver.map
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{X Y : C} →
(f : X ⟶ Y) →
[CategoryTheory.Mono f] → CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)We can map monomorphisms over X to monomorphisms over Y
by post-composition with a monomorphism f : X ⟶ Y.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Overstatement · cited by 935
- CategoryTheory.Monostatement and proof · cited by 893
- CategoryTheory.MonoOverstatement · cited by 115
- CategoryTheory.Over.isMonostatement · cited by 111
- CategoryTheory.Over.mapproof · cited by 97
- CategoryTheory.MonoOver.liftproof · cited by 8
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.Subobject.mapproof · cited by 19
- CategoryTheory.MonoOver.mapIsoproof · cited by 7
- CategoryTheory.MonoOver.mapCompstatement · cited by 3
- CategoryTheory.MonoOver.mapIdstatement · cited by 3
- CategoryTheory.MonoOver.infproof · cited by 2
- CategoryTheory.MonoOver.mapBotstatement · cited by 1
- CategoryTheory.MonoOver.existsIsoMapstatement and proof · cited by 1
- CategoryTheory.MonoOver.mapTopstatement and proof · cited by 1
- CategoryTheory.Subobject.map_pullbackproof · cited by 1
- CategoryTheory.MonoOver.pullbackMapSelfstatement · cited by 1
- CategoryTheory.MonoOver.map.congr_simpstatement and proof · cited by 0
- CategoryTheory.MonoOver.mapIso_counitIsostatement · cited by 0