subgraphs

Stream: Is there code for X?

[Ben Bals]

We are currently working on subgraphs. In particular, If H is a subgraph of G and and M is a subgraph of H, we fail to construct M as a subgraph of G.

Let's put that into Lean's terms. We work on graphs whose vertices are a fintype, i.e.

variables {V: Type*} [fintype V] [decidable_eq V]
variables {G: simple_graph V}

Now, the construction we are trying to define is

def subgraph_in_graph_of_subgraph_in_subgraph_coe
        (H : G.subgraph)
        (M : H.coe.subgraph)
    :
        G.subgraph := sorry

where the resulting subgraph would be the trivial inclusion.

How would we best go about this?

---

Our current state for reference:

def subgraph_in_graph_of_subgraph_in_subgraph_coe
        (H : G.subgraph)
        (M : H.coe.subgraph)
    :
        G.subgraph :=
    {
        verts := subtype.val '' M.verts,
        adj := begin
            intros u v,
            by_cases h_in_M : (u ∈ subtype.val '' M.verts ∧ v ∈ subtype.val '' M.verts),
            {
                have h_u_in_M := h_in_M.1,
                have h_v_in_M := h_in_M.2,
                have h_u_in_H : u ∈ H.verts := by obviously,
                have h_v_in_H : v ∈ H.verts := by obviously,

                let u_H : H.verts := ⟨u, h_u_in_H⟩,
                have h_u_H_in_M : u_H ∈ M.verts,
                focus {
                    have := h_u_in_M,
                    simp at this,
                    cases this with _ h_u_H_in_M,
                    exact h_u_H_in_M,
                },
                let u_M : M.verts := ⟨u_H, h_u_H_in_M⟩,

                let v_H : H.verts := ⟨v, h_v_in_H⟩,
                have h_v_H_in_M : v_H ∈ M.verts,
                focus {
                    have := h_v_in_M,
                    simp at this,
                    cases this with a b,
                    exact b,
                },
                let v_M : M.verts := ⟨v_H, h_v_H_in_M⟩,

                exact M.adj u_M v_M

            },
            { exact false }
        end,
        adj_sub := begin
            intros u v h,
            simp at h,
            by_cases h_in_M : (u ∈ subtype.val '' M.verts ∧ v ∈ subtype.val '' M.verts),
            {
                sorry
            },
            {
                sorry
            }
        end,
        edge_vert := sorry,
        symm := sorry,
    }

[Kyle Miller]

@Ben Bals Here:

/-- Given a subgraph of a subgraph of `G`, construct a subgraph of `G`. -/
@[simps]
def subgraph.coe_subgraph {G' : G.subgraph} (G'' : G'.coe.subgraph) : G.subgraph :=
{ verts := coe '' G''.verts,
  adj := λ v w, ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.adj ⟨v, hv⟩ ⟨w, hw⟩,
  adj_sub := λ v w,
    by { simp_rw [bex_imp_distrib], refine λ _ _ h, G'.adj_sub _, simpa using G''.adj_sub h },
  edge_vert := begin
    simp only [set.mem_image, set_coe.exists, subtype.coe_mk, exists_and_distrib_right,
      exists_eq_right, bex_imp_distrib],
    intros v w hv hw h,
    exact ⟨hv, G''.edge_vert h⟩,
  end }

[Kyle Miller]

Then, using the names of the variables in your definition, if you have M : H.coe.subgraph you can write M.coe_subgraph to get a G.subgraph

[Yaël Dillies]

Is it not just the image under inclusion? You shouldn't need a new definition.

[Kyle Miller]

@Yaël Dillies Do you have a docs link?

[Yaël Dillies]

docs#simple_graph.subgraph.map and we're missing simple_graph.subgraph.inclusion.

[Kyle Miller]

How does simple_graph.subgraph.map apply here? That's the induced injective map on the subgraph relationship, but subgraph.coe_subgraph is about a map on the collections of subgraphs themselves.

[Yaël Dillies]

Oh then it's misnamed. I was expecting it to be the map of a subgraph under a graph hom.

[Kyle Miller]

It's the functor from the lattice of subgraphs to the category of simple graphs, which is why it's called map.

[Yaël Dillies]

Okay, but all other subobjects use map to mean something else.

[Yaël Dillies]

The general way we go about this with subobjects is, if G : simple_graph V, H : subgraph G, then inclusion H : H ->g G and map (inclusion H) : subgraph H -> subgraph G.

[Yaël Dillies]

Here map is the map part of the subgraph functor.

[Kyle Miller]

Presumably you mean subgraph H -> subgraph G here?

[Kyle Miller]

I don't mind if it's renamed to simple_graph.subgraph.inclusion, but in any case we need a new definition since subgraph.coe_subgraph would need map, which doesn't exist yet.

[Yaël Dillies]

Yes, absolutely. I'm just advocating to add the definitions that we use everywhere else, rather than an ad hoc construction.

[Yaël Dillies]

I think subgraph.map should be renamed to subgraph.coe_map, because it is the map of the subgraph.coe functor.

[Yaël Dillies]

Do we have it for other subobjects? Maybe we can get the name from there.

[Kyle Miller]

@Ben Bals Here's an unfinished PR with this construction, in case it's helpful: #14877