Theorems · Definition · category theory
GrpCat.SurjectiveOfEpiAuxs.tau
{A B : GrpCat} → (f : A ⟶ B) → Equiv.Perm (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)Let τ be the permutation on X' exchanging f.hom.range and the point at infinity.
- Defined in
- Mathlib.Algebra.Category.Grp.EpiMono
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 24 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.
- Quiver.Homstatement and proof · cited by 32,603
- SetLike.coeproof · cited by 8,199
- Equiv.Permstatement · cited by 1,375
- MonoidHom.rangeproof · cited by 314
- Equiv.swapproof · cited by 197
- GrpCatstatement and proof · cited by 146
- GrpCat.Hom.homproof · cited by 47
- GrpCat.SurjectiveOfEpiAuxs.XWithInfinitystatement · cited by 22
Cited by8
Results whose statement or proof uses this declaration.
- GrpCat.SurjectiveOfEpiAuxs.hproof · cited by 7
- GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCosetproof · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.h_apply_infinityproof · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCosetstatement · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset'statement · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.τ_apply_infinitystatement · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCosetstatement · cited by 1
- GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinitystatement · cited by 1