Topological spaces

Stream: condensed mathematics

[Adam Topaz]

def Top_to_Condensed : Top ⥤ CondensedSet :=

is now sorry-free (modulo some general stuff about the condensed sheaf condition) in condensed/top_comparison.lean. Still missing is the proof that this is faithful, in case anyone wants to take a look.

[Adam Topaz]

This was easy:

/-- The condensed abelian group associated with a topological abelian group -/
def of_top_ab : Condensed.{u} Ab.{u+1} :=
{ val := of_top_ab.presheaf A ⋙ Ab.ulift.{u+1},
  cond := begin
    rw category_theory.presheaf.is_sheaf_iff_is_sheaf_forget _ _ (forget Ab),
    swap, apply_instance,
    let B := Top.of A,
    change presheaf.is_sheaf _ B.to_Condensed.val,
    exact B.to_Condensed.cond,
  end }

[Johan Commelin]

Was that the sorry that was advertised as -- this one will be hard?

[Adam Topaz]

No, that's the next one ;)

[Johan Commelin]

Oooh, good luck!!

[Adam Topaz]

Yeah, this next one might require additional :coffee:

[Adam Topaz]

done

def to_Condensed : CompHausFiltPseuNormGrp₁.{u} ⥤ Condensed.{u} Ab.{u+1} :=
{ obj := λ A,
  { val := Presheaf A ⋙ Ab.ulift.{u+1},
    cond := Presheaf_comp_ulift_is_sheaf _ },
  map := λ A B f, ⟨whisker_right (Presheaf.map f) _⟩,
  map_id' := λ X, by { ext : 2, dsimp, simp },
  map_comp' := λ X Y Z f g, by { ext : 2, dsimp, simp } }

There is some golfing room with this proof, if anyone wants to take a look.

[Johan Commelin]

What did you put into your coffee :open_mouth: ?

[Adam Topaz]

I still have 1/2 a cup left.

[Adam Topaz]

But that has to be reserved for my office hours...

[Adam Topaz]

I suppose we will need the functor from CompHausFiltPseuNormGrp (without the 1) as well, but the proof of the sheaf condition should be identical. So once we have the underlying presheaf, we could just reuse Presheaf_comp_ulift_is_sheaf.

[Adam Topaz]

Adam Topaz said:

I suppose we will need the functor from CompHausFiltPseuNormGrp (without the 1) as well, but the proof of the sheaf condition should be identical. So once we have the underlying presheaf, we could just reuse Presheaf_comp_ulift_is_sheaf.

I just did this, so now we have the following two defs:

def CompHausFiltPseuNormGrp.to_Condensed : CompHausFiltPseuNormGrp.{u} ⥤ Condensed.{u} Ab.{u+1} :=
{ obj := λ A,
  { val := Presheaf A ⋙ Ab.ulift.{u+1},
    cond := Presheaf_comp_ulift_is_sheaf _ },
  map := λ A B f, ⟨whisker_right (Presheaf.map f) _⟩,
  map_id' := λ X, by { ext : 2, dsimp, simp },
  map_comp' := λ X Y Z f g, by { ext : 2, dsimp, simp } }

def CompHausFiltPseuNormGrp₁.to_Condensed :
  CompHausFiltPseuNormGrp₁.{u} ⥤ Condensed.{u} Ab.{u+1} :=
CompHausFiltPseuNormGrp₁.enlarging_functor ⋙ CompHausFiltPseuNormGrp.to_Condensed

This should take care of the node CHPNG-to-cond on the dep. graph.

[Johan Commelin]

I'll update it

[Johan Commelin]

ooh, you already did. So I added a \leanok