extr disc projective in CompHaus

Stream: condensed mathematics

[Johan Commelin]

Do we already have a proof that extremally disconnected spaces are projective in CompHaus?
By definition (in Lean) they are projective in Profinite.

[Reid Barton]

do you have a math proof?

[Johan Commelin]

Not yet.

[Johan Commelin]

The definition in Analytic.pdf is that every surjection from a comp-haus splits. So then it would be easy.

[Johan Commelin]

And $\beta(X)$ would still be extr.disc in that sense.

[Johan Commelin]

So maybe we should just refactor the definition.

[Reid Barton]

You could also define it as a retract of $\beta$ of something, or as compact Hausdorff $X$ s.t. $\beta X \to X$ splits

[Reid Barton]

I think the math proof of your original question would be something like--if $X$ is projective in Profinite then $X$ lifts against $\beta X \to X$ so $X$ is a retract of $\beta X$, now check that $\beta S$ is projective in CompHaus and so a retract is too

[Reid Barton]

which does suggest you might start from another definition though it doesn't really matter

[Johan Commelin]

Yeah, I just drew that diagram (-;

[Reid Barton]

I still like this idea that it's preferable to avoid quantifying over Type in definitions

[Reid Barton]

(Because then the definition is "obviously" universe-independent.)

[Reid Barton]

Here's a fun example I just thought of. Let's call a group G : Type u "lonely" if Type u doesn't contain an inaccessible cardinal. That's some property of the form forall X : Type u, [moderately long statement involving functions between subsets of X and so on]. We can't prove that if G is lonely, then ulift G is lonely.

[Reid Barton]

And it's not really obvious why being projective isn't a property like this, if you define it by a lifting condition.

[Johan Commelin]

Refactoring the defn was too annoying for now. So I just proved the lifting lemma.

[Adam Topaz]

I hope most of the stuff available in condensed/extr should "just work" if you have the right lift and lift_lifts lemmas... so I hope (eventually) refactoring shouldn't be too much of an issue.

[Johan Commelin]

We will need

lemma exact_iff_ExtrDisc  {A B C : Condensed.{u} Ab.{u+1}} (f : A ⟶ B) (g : B ⟶ C) :
  exact f g ↔ ∀ (S : ExtrDisc),
    exact (f.1.app $ ExtrDisc_to_Profinite.op.obj (op S))
          (g.1.app $ ExtrDisc_to_Profinite.op.obj (op S)) :=
sorry

But besides that

lemma exact_of_exact_with_constant {A B C : CompHausFiltPseuNormGrp₁.{u}}
  (f : A ⟶ B) (g : B ⟶ C) (Cf : ℝ≥0) (hCf : 1 ≤ Cf)
  (hfg : exact_with_constant f g Cf) :
  exact (to_Condensed.map f) (to_Condensed.map g) :=

is now done.

[Adam Topaz]

Yeah, that should go through the equivalence with ExtrSheafProd (or whatever I called it...).

[Adam Topaz]

I can have a go at it later.

[Johan Commelin]

Thanks!

[Adam Topaz]

lemma exact_iff_ExtrDisc {A B C : Condensed.{u} Ab.{u+1}} (f : A ⟶ B) (g : B ⟶ C) :
  exact f g ↔ ∀ (S : ExtrDisc),
    exact (f.1.app $ ExtrDisc_to_Profinite.op.obj (op S))
          (g.1.app $ ExtrDisc_to_Profinite.op.obj (op S)) :=

is sorry-free