Theorems · Theorem · category theory

Profinite.exists_lift_of_finite_of_injective_of_surjective

∀ {X : Type u_1} {Y : Type u_2} {S : Type u_3} {T : Type u_4} [inst : TopologicalSpace X] [CompactSpace X]
  [inst_2 : TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] [inst_6 : TopologicalSpace S]
  [T2Space S] [Finite S] [inst_9 : TopologicalSpace T] [T2Space T] (f : X → Y),
  Continuous f →
    Function.Injective f →
      ∀ (f' : S → T),
        Function.Surjective f' →
          ∀ (g : X → S),
            Continuous g → ∀ (g' : Y → T), Continuous g' → g' ∘ f = f' ∘ g → ∃ k, Continuous k ∧ f' ∘ k = g' ∧ k ∘ f = g

This is the key statement for the inductive proof of injectivity of light profinite spaces. Given a commutative square `` X >-f-> Y |g |g' v v S -f'->> T ` where Y is profinite, S is finite, f is injective and f' is surjective, there exists a diagonal map k : Y → S` making the diagram commute.

Defined in

Mathlib.Topology.Category.LightProfinite.Injective

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpaceTopologicalSpaceCompactSpaceT2SpaceTotallyDisconnectedSpaceTopologicalSpaceT2SpaceFiniteTopologicalSpaceT2Space