Theorems · Theorem · category theory

Profinite.exists_lift_of_finite_of_mono_of_epi

∀ {X Y S T : Profinite} [Finite ↑S.toTop] (f : X ⟶ Y) [CategoryTheory.Mono f] (f' : S ⟶ T) [CategoryTheory.Epi f']
  (g : X ⟶ S) (g' : Y ⟶ T),
  CategoryTheory.CategoryStruct.comp f g' = CategoryTheory.CategoryStruct.comp g f' →
    ∃ k, CategoryTheory.CategoryStruct.comp k f' = g' ∧ CategoryTheory.CategoryStruct.comp f k = g

A categorically stated version of exists_lift_of_finite_of_injective_of_surjective in the category Profinite.

Defined in: Mathlib.Topology.Category.LightProfinite.Injective
Cited by: 0 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Finite CategoryTheory.Mono CategoryTheory.Epi

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CategoryTheory.ConcreteCategory.homproof · cited by 4,022
TopCat.carrierstatement and proof · cited by 3,184
Finitestatement and proof · cited by 3,029
Continuousproof · cited by 2,592
TopCatstatement and proof · cited by 1,889
CategoryTheory.Monostatement and proof · cited by 893
CategoryTheory.Epistatement and proof · cited by 688
CategoryTheory.comp_applyproof · cited by 387
TotallyDisconnectedSpacestatement and proof · cited by 295

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.