TFAE fam of epis

Stream: Copenhagen Masterclass 2023

[Boris Kjær]

Here's to work on TFAE statement regarding finite families of epimorphisms in ProFinite and ExtrDisc

[Boris Kjær]

Created branch bbolvig/families-of-effective-epis

[Riccardo Brasca]

Can you push a sorried statement? We need it to prove that Profinite is precoherent

[Riccardo Brasca]

Well, in practice we are doing the same thing... are you working on it?

[Boris Kjær]

yes, the statement has been added in Profinite/Epi.lean

[Boris Kjær]

Is that working for you guys?

[Riccardo Brasca]

Yes thanks

[Riccardo Brasca]

For profinite

variable {X Y B : Profinite.{u}} (f : X ⟶ B) (g : Y ⟶ B)

/--
The pullback of two morphisms `f,g` in `Profinite`, constructed explicitly as the set of
pairs `(x,y)` such that `f x = g y`, with the topology induced by the product.
-/
def pullback : Profinite.{u} :=
  letI set := { xy : X × Y | f xy.fst = g xy.snd }
  haveI : CompactSpace set := by
    rw [← isCompact_iff_compactSpace]
    apply IsClosed.isCompact
    exact isClosed_eq (f.continuous.comp continuous_fst) (g.continuous.comp continuous_snd)
  Profinite.of set

works

[Riccardo Brasca]

I think you also need it

[Jon Eugster]

totally golfed code ;)

  intro x hx y hy
  unfold Set.Subsingleton at h
  have a₁ : (f.inv x) ∈ ↑f.hom ⁻¹' t
  · rw [Set.mem_preimage]
    simpa
  have a₂ : (f.inv y) ∈ ↑f.hom ⁻¹' t
  · rw [Set.mem_preimage]
    simpa
  specialize h a₁ a₂
  replace h := congr_arg f.hom h
  simp at h
  assumption

[Jon Eugster]

Template with the statements:
https://github.com/adamtopaz/CopenhagenMasterclass2023/pull/9

@Riccardo Brasca

[Riccardo Brasca]

Thanks!