condensed/acyclic

Stream: condensed mathematics

[Johan Commelin]

Apart of exactness of a certain complex, this file now contains only two SELFCONTAINED sorries.
One is:

-- SELFCONTAINED
lemma cochain_complex.mono_of_is_zero_homology_0
  {𝓐 : Type*} [category 𝓐] [abelian 𝓐]
  (C : cochain_complex 𝓐 ℕ) (h : is_zero $ C.homology 0) :
  mono (C.d 0 1) :=
begin
  sorry
end

The other is about applying an additive functor to the alternating face map complex of a simplicial object.

[Filippo A. E. Nuccio]

I have 100 copies to correct on my desk and some stuff to do on the blueprint, so most probably others will be faster than me. If not, I will be happy to take this one if needed, or anything that will be left once I will emerge from my marking adventure.

[Johan Commelin]

Good luck with grading!

[Riccardo Brasca]

I've finishing my grading so I can to it :D

[Riccardo Brasca]

It's done.

[Adam Topaz]

I assume no one is working on the following?

lemma free_Cech_exact (F : arrow Profinite.{u}) (n : ℤ) :
  is_zero $ (free_Cech F).homology n :=
sorry

I'll try to get that sorry done in the next couple of days.

[Johan Commelin]

I'm not working on that atm

[Johan Commelin]

Btw, see

lemma acyclic_of_exact.induction_step_ex₃

for (roughly) how to reduce it exactness of free_Cech'.

[Adam Topaz]

I added various self-contained sorries in for_mathlib/chain_complex_exact.

[Adam Topaz]

A few additional selfcontained sorries can now be found in condensed/adjunctions. They are just some lemmas about additivity of certain functors.

[Kevin Buzzard]

OK I am finally getting to this stuff!

[Kevin Buzzard]

I'll take a look at condensed/adjunctions.

[Kevin Buzzard]

There's only one sorry -- some statement that a functor is preadditive. I'll try that now

[Adam Topaz]

@Kevin Buzzard that sorry is a special case of one in for_mathlib/abelian_sheaves/exact

[Adam Topaz]

(sheafification is additive)

[Adam Topaz]

But for silly universe reasons it's possible that TC search won't find the one in condensed/adjunctions automatically :(

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

Oh I got nothing done, I got distracted by other things :-/

[Adam Topaz]

The main argument for

lemma free_Cech_exact (F : arrow Profinite.{u}) (hF : function.surjective F.hom) : ∀ (n : ℤ),
  is_zero $ (free_Cech F).homology n :=

is now done, moodulo various sorries that should be more self-contained.

[Adam Topaz]

Note that the assumption (hF : function.surjective F.hom) was added, so some stuff may break, but this is a necessary assumption.

[Johan Commelin]

Ooh thanks for catching that missing assumption. It's certainly satisfied when we use this lemma.

[Adam Topaz]

Unfortunately...... we seem to be missing the comparbility of docs#category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting with docs#category_theory.presheaf_to_Sheaf

[Adam Topaz]

We need that for these sorries
https://github.com/leanprover-community/lean-liquid/blob/47a989b746f9e3d0e56dd3c65101c53f9b944004/src/condensed/acyclic.lean#L93

[Johan Commelin]

What does it take to add that? Is this a sizable gap?

[Adam Topaz]

Okay, I think there may be a slick way to do with by playing around with some right Kan extensions.

[Adam Topaz]

def ExtrDisc_sheafification_iso :
  (whiskering_left _ _ _).obj ExtrDisc_to_Profinite.op ⋙
  presheaf_to_Sheaf ExtrDisc.proetale_topology Ab.{u+1} ≅
  presheaf_to_Sheaf proetale_topology _ ⋙ (Condensed_ExtrSheaf_equiv _).inverse :=
begin
  let A1 : (whiskering_left _ _ Ab.{u+1}).obj ExtrDisc_to_Profinite.{u}.op ⊣ _ :=
    Ran.adjunction _ _,
  let A2 : presheaf_to_Sheaf ExtrDisc.proetale_topology Ab.{u+1} ⊣ _ :=
    sheafification_adjunction _ _,
  let B1 : presheaf_to_Sheaf proetale_topology Ab.{u+1} ⊣ _ :=
    sheafification_adjunction _ _,
  let B2 : (Condensed_ExtrSheaf_equiv Ab.{u+1}).inverse ⊣ _ :=
    equivalence.to_adjunction _,
  let A := A1.comp _ _ A2,
  let B := B1.comp _ _ B2,
  exact A.nat_iso_of_right_adjoint_nat_iso B ExtrDisc_sheafification_iso_aux,
end

I'm a little surprised at how easy that was.

[Adam Topaz]

I think I'll go ahead and open a mathlib PR for this one.

[Adam Topaz]

#14512

[Adam Topaz]

I know we probably won't bump mathlib in LTE any time soon, so I'll add these changes to the LTE repo directly as well.

[Adam Topaz]

In particular, the lemma pullback_sheafification_compatibility_hom_apply_val wiill probably be needed for the followiing sorry:
https://github.com/leanprover-community/lean-liquid/blob/c0531fb0e89511ecfa9b5feda9c873a951f74f12/src/condensed/acyclic.lean#L93

[Kevin Buzzard]

Not bumping mathlib: Is that right? I can't get to mathlib right now because I'm on a train in a foreign country and my internet is being throttled. But I just noticed that category_theory.limits.kernel_comparison_comp_ι is not as universe polymorphic as I might have expected: there's a functor between two categories and these two categories have morphisms in the same universe. I use this to prove homology_zero_iff_map_homology_zero which then inherits the universe restriction.

Is the plan now to not bump mathlib until we're at the end? Is the idea that it's now too hard to bump mathlib because of changes in category theory?

[Adam Topaz]

This was probably because not too long ago limits in a category C : Type u with [category.{v} C] had to be indexed by a small category J : Type v (so category.{v} J). That means that in order to phrase that a functor preserves liimits, we had to ensure that the source and target category of the functor had morphisms in the same universe level.

[Adam Topaz]

Do you think this particular case of a kernel will cause issues in LTE?

[Adam Topaz]

I think your exact_iff_map_exact could probably be done without a universe restriction.
I'm about to go into a meeting, but I'll try too generalize soon.

[Adam Topaz]

(and it seems that II also need to clean out my keeeeyyyyyyboard)

[Kevin Buzzard]

I'm just filling in the selfcontained sorries, I don't know if the restriction will cause problems.

[Adam Topaz]

This lemma is used to pass between homomology in abellian sheaves on Profinite to homology in abelian sheaves on ExtrDisc, and both categories of sheaves should have the same universe levels. I think it's okay to leave things as is for now.

[Johan Commelin]

Kevin Buzzard said:

Is the plan now to not bump mathlib until we're at the end? Is the idea that it's now too hard to bump mathlib because of changes in category theory?

Yes, that's my hunch. But I think it should be fine. Once we reach :checkered_flag: we can start thinking about reorganizing things, cleaning up, bumping mathlib, PRing things, etc...

[Adam Topaz]

I'm quite certain we'll make it to the finish line without a bump. I can see the end in sight.

[Yaël Dillies]

Is PRing to mathlib still on the radar?

[Kevin Buzzard]

Feel free to PR stuff in for_mathlib!

[Adam Topaz]

I think once LTE is done, we'll have a lot of "fun" clearing out the for_mathlib folder.

[Kevin Buzzard]

If perfectoid is anything to go by, nobody will clear it out and it will rot.

[Adam Topaz]

One more sorry left in this:

--TODO: This relates the above construction to AddcommGroup.homology_map
-- the above def has more convenient defeq properties for some of the proofs below, but
-- the `AddCommGroup.homology_map` is better suited for `aux₂_naturality`.
lemma map_explicit_homology_eq
  {P₁ P₂ : bounded_homotopy_category C} (f : P₁ ⟶ P₂) (B : C) (i : ℤ) :
  map_explicit_homology f B i =
  AddCommGroup.homology_map
    ((hom_complex P₂ B i).d_comp_d _ _ _)
    ((hom_complex P₁ B i).d_comp_d _ _ _)
    (commsq.of_eq $ ((map_hom_complex f B i).comm (i+1) i).symm)
    (commsq.of_eq $ ((map_hom_complex f B i).comm i (i-1)).symm) :=
sorry

This relates the somewhat nonexplicit AddCommGroup.homology_map to a more explicit one defined in terms of actual elements.

[Kevin Buzzard]

Hey you know all the cool kids are using has_homology.map now? Maybe it helps here?

[Adam Topaz]

did you see my homology_map_eq?

[Kevin Buzzard]

no not yet -- where?

[Adam Topaz]

the has_homology file

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/aed9785900dd54c8a1432c73f62cdeaae0e997a7/src/for_mathlib/has_homology.lean#L258

[Adam Topaz]

I saw you added something similar as well.

[Adam Topaz]

The whole point of that sorry above is to relate a has_homology.map construction to something explicit.

[Kevin Buzzard]

I think we've now got two different ways of solving the problem that working with homology.map was difficult.

[Kevin Buzzard]

You've related it to has_homology.map between the homology objects and I've related it to a more general has_homology.map coming from the isomorphism you can cook up between homology f g and any other object H satisfying has_homology f g H

[Adam Topaz]

I think the proof of your lemma would could be roughly by simp [homology_map_eq].

[Adam Topaz]

Well, not quite, but close

lemma has_homology.map_iso_homology_map :
has_homology.map h₁ h₂ sq1 sq2 = (has_homology.iso h₁ (homology.has f₁ g₁ h₁.w)).hom ≫
  (homology.map h₁.w h₂.w ⟨α, β, sq1.w.symm⟩ ⟨β, γ, sq2.w.symm⟩ rfl) ≫
  (has_homology.iso h₂ (homology.has f₂ g₂ h₂.w)).inv:=
begin
  erw homology_map_eq,
  apply h₁.ext_π,
  apply h₂.ext_ι,
  simp,
end

There should be a variant of homology_map_eq which uses an actual hom in arrow like you had it set up as opposed to arrow.hom_mk, but otherwise this proof is the usual thing we do in the category theory library, i.e. start with ext or some variant, then simplify.

[Adam Topaz]

Overall I think the has_homology api is pretty smooth. My only complaint is that I would like the structure not to rely on epi_desc and mono_lift and kernel/cokernel, and instead allow for some arbitrary (co)limit (co)cones for the associated diagrams so that we can have nice defeq properties in explicit variants of homology (such as the one for AddCommGroup).

[Adam Topaz]

Alright, condensed/acyclic should be sorry-free now

[Kevin Buzzard]

Hopefully imker will be sorry-free tomorrow (I think i know how to prove it given what we have)

[Johan Commelin]

Adam Topaz said:

Alright, condensed/acyclic should be sorry-free now

Wow!! That was quite a battle in the end, all those naturality proofs. Thank you so much! I'm going to update the dependency graph.

[Johan Commelin]

The graph has been updated. Four items left!