[Merged by Bors] - feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths

[bottine]

Co-authored-by: Antoine Labelle antoinelab01@gmail.com

---

• depends on: [Merged by Bors] - feat(combinatorics/quiver/*): More edge reversal constructions #17665

[YaelDillies]

untested

Suggested change

	{ induction x₀, induction x₁, rintro ⟨h, H⟩, cases h, cases H,
	{ induction x₀,
	induction x₁,
	rintro ⟨rfl, ⟨⟩⟩,

[bottine]

Doesn't work, not sure why.

[YaelDillies]

Suggested change

	{ induction x₀, induction x₁, rintro ⟨h, H⟩, cases h, cases H,
	{ induction x₀,
	induction x₁,
	rintro ⟨rfl, rfl⟩,

maybe?

[bottine]

nope :)

[bottine]

I'm waiting for the CI to pass, but I can do

lemma ext_iff' {x₀ x₁ : sigma β} :
  x₀ = x₁ ↔ ∃ h : x₀.1 = x₁.1, h.rec_on x₀.2 = x₁.2 :=
begin
  split,
  { rintro ⟨⟩,
    exact ⟨rfl, rfl⟩, },
  { induction x₀,
    induction x₁,
    rintros ⟨h, H⟩,
    cases h,
    cases H,
    refl, }
end

if that's worth it? It's just one tactic per line, and refl instead of simp…

[bottine]

@YaelDillies can you only "approve", or also put it on the maintainer queue? That would be nice

[YaelDillies]

Instead of assuming that there are inverses to the φ.star u and φ.costar u and showing that there's an inverse to the φ.path_star u, can you instead construct the inverses to the φ.path_star u from inverses for the φ.star u and φ.costar u?

[bottine]

Probably can, but what's the gain? I guess it will make for a cleaner proof, let me see.

[YaelDillies]

Yeah, I'm hoping for a cleaner proof. But I don't know how much it will make you change your framework.

[bottine]

I'll try for a bit and see if helps and is reasonably easy, and give up otherwise.

[bottine]

Edit. Got it down to this, and I think we won't get a shorter proof in the end, even though it might be a bit cleaner. I think I'll give that up, if it's not something crucial in your mind.

noncomputable! def prefunctor.path_star_bijective_aux
  {ψ : ∀ u, quiver.star (φ.obj u) → quiver.star u} (ψr : ∀ u, right_inverse (ψ u) (φ.star u)) :
  ∀ u (p : quiver.path_star (φ.obj u)), { q : quiver.path_star u // φ.path_star u q = p }
| u ⟨_, quiver.path.nil⟩ := ⟨⟨u, quiver.path.nil⟩, rfl⟩
| u ⟨v', @quiver.path.cons _ _ _ v v'' p e⟩ :=
  let
    hh := prefunctor.path_star_bijective_aux _ ⟨_, p⟩,
    f : quiver.star hh.val.1 := ψ _ ⟨v', e.cast (sigma.ext_iff'.mp hh.property).some.symm rfl⟩
  in
    ⟨ ⟨_, hh.val.2.cons f.2,⟩, by
      begin
        dsimp [f, hh], clear f hh,
        obtain ⟨⟨u', q⟩, h⟩ := prefunctor.path_star_bijective_aux _ ⟨_, p⟩,
        obtain ⟨rfl, rfl⟩ := h,
        let h := ψr u' ⟨_, e⟩,
        rw [sigma.ext_iff'] at h ⊢,
        obtain ⟨h', _⟩ := h,
        change ∃ (h : φ.obj _ = _), path.cast rfl h _ = _,
        refine ⟨h', _⟩,
        simpa only [path.cast_cons, path.cast_rfl_rfl, eq_self_iff_true, heq_iff_eq, true_and],
      end ⟩

[YaelDillies]

To me it looks like you could be creating the equivalence instead of proving bijectivity. What happens if you make is_covering data?

structure prefunctor.covering :=
(star_equiv : Π u, quiver.star u ≃ quiver.star (φ.obj u))
(costar_equiv : Π u, quiver.costar u ≃ quiver.costar (φ.obj u))

[bottine]

Well, that specifically won't work, since you're just giving equivalences, and not proving that \phi.star and \phi.costar are part of equivalences.
But assuming we had a structure giving data for being a covering, I'm not sure we would get much shorter proofs, since most of it is about dealing with equalities of endpoints.

[YaelDillies]

My question was mostly whether you really wanted is_covering to be a Prop, rather than bundling the inverse as equiv does.

[bottine]

Yeah. I don't really know but:

• As I said, I feel like most of the length in proofs comes from having to deal with equalities of indices/vertices rather than the "prop instead of data" choice.
• Inverses are unique, since the forward function is given, so I don't feel like bundling them would provide much.
  I've used this implementation a bit more here (see the bottom of the covering file) and it seems to work well enough as-is.

[YaelDillies]

Okay, but the inverse of an equiv is unique too, but we still give the inverse explicitly. Would you mind splitting is_covering to another PR? I'm happy with the rest.

[bottine]

So, only keep the star/costar stuff?

[YaelDillies]

Let's ask for other people's opinions.
cc @kmill, @b-mehta

[kim-em]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests