Theorems · Definition · category theory

GrpCat.SurjectiveOfEpiAuxs.g

{A B : GrpCat} → (f : A ⟶ B) → ↑B →* Equiv.Perm (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)

Let g : B ⟶ S(X') be defined as such that, for any β : B, g(β) is the function sending point at infinity to point at infinity and sending coset y to β • y.

Defined in

Mathlib.Algebra.Category.Grp.EpiMono

Cited by

8 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound