Theorems · Theorem · group theory
CategoryTheory.Subgroupoid.le_comap_map
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
(φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) (S : CategoryTheory.Subgroupoid C),
S ≤ CategoryTheory.Subgroupoid.comap φ (CategoryTheory.Subgroupoid.map φ hφ S)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Groupoidstatement and proof · cited by 182
- CategoryTheory.Subgroupoidstatement and proof · cited by 75
- GaloisConnection.le_u_lproof · cited by 52
- CategoryTheory.Subgroupoid.mapstatement · cited by 10
- CategoryTheory.Subgroupoid.comapstatement · cited by 8
- CategoryTheory.Subgroupoid.galoisConnection_map_comapproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.