TopCatLemma [stacks 08ZH]

[haowen214]

Finished the proof of [stacks 08ZH] (isClosedEmbedding_pullback_to_prod)

I have a small question of one part, which seems to be a lemma already in Mathlib but doesn't seem to match the universe level, so I just adapted the proof lines rather than applying the lemma, but I don't know if there is a better way that I should do it? (See my comments inside the file)

[chrisflav]

The issue here is that the TopCat.range_pullback_to_prod lemma has bad universe generality (in fact, Lean inferred the universe in TopCat to be 0). This needs to be fixed in mathlib.

[haowen214]

I guess they should've wrriten {X Y Z : TopCat.{u}} insteand of {X Y Z : TopCat} there right?

[chrisflav]

Yes, to be safe. Universe unification does not always have a unique solution, so I think the algorithm sometimes applies some heuristics. If you get lucky, it gets it right, but here it seems we don't get lucky.

[chrisflav]

BTW, I made #38779 to fix the issue in mathlib and it is merged now, so the next time when I update this repository to the latest mathlib version, I'll remove the TODO.

[chrisflav]

Thanks for contributing to this project! I have made a suggestion below. You can just put the two additional lemmas above this lemma in the same file.

Looking forward to more contributions! :)

[chrisflav]

Here is a golfed version of your proof. Mathematically, it is exactly the same. I just rephrased things a bit, to make them more compact.

Suggested change

	Topology.IsClosedEmbedding ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) := by
	set f1 := ConcreteCategory.hom f
	set g1 := ConcreteCategory.hom g
	constructor
	· exact isEmbedding_pullback_to_prod f g
	· have s1 : Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) = (homeoOfIso (prodIsoProd X Y)) ⁻¹' (Prod.map ⇑f1 ⇑g1 ⁻¹' Set.range fun x ↦ (x, x)) := by
	ext x
	simp
	constructor
	· rintro ⟨a, ha⟩
	rw[← ha]
	have hp := pullbackIsoProdSubtype f g
	have : ((homeoOfIso (X.prodIsoProd Y)) ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) a)).1 = ((prod.lift (pullback.fst f g) (pullback.snd f g)) ≫ (X.prodIsoProd Y).hom ≫ TopCat.prodFst ) a := rfl
	rw[this]
	simp only [prodIsoProd_hom_fst, limit.lift_π, BinaryFan.mk_pt, BinaryFan.mk_fst]
	have : ((homeoOfIso (X.prodIsoProd Y)) ((ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g))) a)).2 = ((prod.lift (pullback.fst f g) (pullback.snd f g)) ≫ (X.prodIsoProd Y).hom ≫ TopCat.prodSnd ) a := rfl
	rw[this]
	simp [f1, g1]
	rw[← ConcreteCategory.comp_apply]
	simp[pullback.condition]
	· intro ha
	-- For this part, there is a mathlib lemma "range_pullback_to_prod", but if we want to apply that lemma, we see that in this lemma we have 'TopCat: Type 1', but we are in 'TopCat : Type (u + 1)' so Lean shows a mismatch and cannot state 'range_pullback_to_prod f g' for our f and g. But since the proof lines are essentially the same, I just adapted the original proof lines below. I don't know if there is a better way of doing it. -- Haowen
	use (pullbackIsoProdSubtype f g).inv ⟨(X.prodIsoProd Y).hom x , ha⟩
	apply Concrete.limit_ext
	rintro ⟨⟨⟩⟩ <;>
	rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
	-- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
	cat_disch
	have hfg := Continuous.prodMap (map_continuous f1) (map_continuous g1)
	have hc := IsClosed.preimage hfg (t2Space_iff_diagonal_closed.mp ‹T2Space Z›)
	have hc1 := (TopCat.homeoOfIso (TopCat.prodIsoProd X Y)).isClosed_preimage.mpr hc
	rw[← s1] at hc1
	exact hc1
	refine ⟨isEmbedding_pullback_to_prod f g, ?_⟩
	suffices s1 : Set.range (prod.lift (pullback.fst f g) (pullback.snd f g)) =
	(homeoOfIso (prodIsoProd X Y)) ⁻¹' (Prod.map f.hom g.hom ⁻¹' Set.range fun x ↦ (x, x)) by
	rw [s1, (TopCat.homeoOfIso (TopCat.prodIsoProd X Y)).isClosed_preimage]
	exact .preimage (.prodMap (map_continuous f.hom) (map_continuous g.hom))
	(t2Space_iff_diagonal_closed.mp ‹T2Space Z›)
	ext x
	simp only [Set.mem_range, Set.range_diag, Set.mem_preimage, Set.mem_diagonal_iff, Prod.map_fst,
	Prod.map_snd]
	constructor
	· rintro ⟨a, rfl⟩
	rw [← TopCat.prodFst_apply, ← TopCat.prodSnd_apply, homeoOfIso_apply]
	simp only [← ConcreteCategory.comp_apply]
	simp [pullback.condition]
	· intro ha
	-- TODO: replace this by `range_pullback_to_prod` after updating mathlib
	use (pullbackIsoProdSubtype f g).inv ⟨(X.prodIsoProd Y).hom x , ha⟩
	apply Concrete.limit_ext
	rintro ⟨⟨⟩⟩ <;>
	rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, limit.lift_π] <;>
	-- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
	cat_disch

As you can see, this relies on adding two new lemmas:

lemma TopCat.prodFst_apply {X Y : TopCat.{u}} (x : X × Y) : TopCat.prodFst x = x.1 := by
  rfl

lemma TopCat.prodSnd_apply {X Y : TopCat.{u}} (x : X × Y) : TopCat.prodSnd x = x.2 := by
  rfl

(these are the two I mentioned last Wednesday)

A few things to note:

• If you have one long have and the main proof quickly follows from that, consider restructuring it into a suffices as above. It gets rid of a long indented block and it is also a bit easier to follow I find.
• If you are proving two things with constructor, but one of the proofs is very short, consider using refine ⟨short_proof, ?_⟩. This also gets rid of a long indented block.
• I have also adapted the mathlib style everywhere, which for example says rw[h] should be rw [h] (note the additional space), but this is of course a very minor point.

I hope this is useful for you, please don't take it as a discouragement that the proof can be golfed a bit :)