2-step proj resolution (PID)

Stream: condensed mathematics

[Fabian Glöckle]

I am trying to prove the existence of 2-step projective resolutions of modules over PIDs using the "submodules of free modules are free" statement.
I could produce P : chain_complex (Module.{v} R) ℕand π : P ⟶ ((chain_complex.single₀ (Module.{v} R)).obj (of R M)) and prove projectivity of all elements of P, but am currently stuck proving exactness.

My problem is mainly that P is defined using two nested ite. Therefore, when proving exactness at high degrees, the goal has the perfectly innocent form category_theory.exact 0 0 (with zero morphisms between zero objects) and could math-wise be closed using category_theory.exact_of_zero (f : A ⟶ 0) (g : 0 ⟶ C) : category_theory.exact f g. However, the middle element is

ite (n + 2 = 0) (of R (M →₀ R)) (ite (n + 2 = 1) (of R ↥((free_module_natural_map R M).ker)) 0)

in the presence of hn : n = 1, and not defeq to the zero required by category_theory.exact_of_zero.

Would you recommend proving propositionally that the term above equals zero, and rewriting / casting along that proof, or give up on equality rewriting and instead use category_theory.preadditive.exact_of_iso_of_exact and prove that there exists an iso to 0 -> 0 -> 0using the same proofs?

I am asking because I assume you have had to deal with lots of such defeq / propeq problems in the homological algebra library. Otherwise, I will just try out both approaches and see which one succeeds first :)

[Fabian Glöckle]

does is_zero_object help here?

[Fabian Glöckle]

replacement_nat?

[Riccardo Brasca]

We have preadditive.exact_of_iso_of_exact' somewhere in the LTE, that is slightly more usable than the version in mathlib. I would use that.

[Fabian Glöckle]

Yes!

This works for the high degrees, but I cannot get exactness at degree 1 (the only interesting one) with the same approach:

The sequences look like
0 -> ker -> RM
and
0 -> ker' -> (RM)',
where the primed versions are the ones with iteinside.

When applying preadditive.exact_of_iso_of_exact', I prove ker ≅ ker'and RM ≅ (RM)' by rewriting iso.refl which gives the commutative square ker -> RM -> (RM)' = ker -> ker' -> (RM)'which cannot be shown to commute because three of its four edges are casts.

[Fabian Glöckle]

I could replace the module ker by the category theoretical kernel, then exactness should be for free.
But I fear this shifts the problem over to proving projectivity of kernel...

[Johan Commelin]

@Fabian Glöckle Isn't it easier to use the equation compiler instead of ite?

[Johan Commelin]

def X (M : AddCommGroup) : ℕ → AddCommGroup
| 0 := free_abelian_group M
| 1 := ker blabla
| (n+2) := 0

[Johan Commelin]

There is AddCommGroup.exact_iff somewhere in LTE. That would reduce you to the "normal" range and ker for additive group homs.

[Johan Commelin]

src/for_mathlib/AddCommGroup/exact.lean
12:theorem exact_iff : exact f g ↔ f.range = g.ker :=

[Kevin Buzzard]

Yes, Amelia taught me this trick when making small complexes -- the defeqs are much better if you use the equation compiler. But of course at some point we're going to have to figure out how to do this.