[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
v : V
⊢ Set.Finite (SimpleGraph.singletonSubgraph G v).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ Set.Finite (subgraphOfAdj G e).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e
[PROOFSTEP]
simp [singletonFinsubgraph, finsubgraphOfAdj]
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : Adj G u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e
[PROOFSTEP]
simp [singletonFinsubgraph, finsubgraphOfAdj]
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
⊢ G'' →fg F
[PROOFSTEP]
refine' ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, _⟩
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
⊢ ∀ {a b : ↑(↑G'').verts},
    Adj (Subgraph.coe ↑G'') a b →
      Adj F
        ((fun x =>
            match x with
            | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
          a)
        ((fun x =>
            match x with
            | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
          b)
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩ huv
[GOAL]
case mk.mk
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
G' G'' : Finsubgraph G
h : G'' ≤ G'
f : G' →fg F
u : V
hu : u ∈ (↑G'').verts
v : V
hv : v ∈ (↑G'').verts
huv : Adj (Subgraph.coe ↑G'') { val := u, property := hu } { val := v, property := hv }
⊢ Adj F
    ((fun x =>
        match x with
        | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
      { val := u, property := hu })
    ((fun x =>
        match x with
        | { val := v, property := hv } => RelHom.toFun f { val := v, property := (_ : v ∈ (↑G').verts) })
      { val := v, property := hv })
[PROOFSTEP]
exact f.map_rel' (h.2 huv)
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
⊢ Nonempty (G →g F)
[PROOFSTEP]
cases nonempty_fintype W
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
⊢ Nonempty (G →g F)
[PROOFSTEP]
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' => ⟨h G'.unop G'.unop.property⟩
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
[PROOFSTEP]
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') :=
  by
  intro G'
  haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
  haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
  exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
intro G'
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
[PROOFSTEP]
classical exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
[PROOFSTEP]
exact Pi.fintype
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this✝ : Fintype ↑(↑G'.unop).verts
this : Fintype (↑(↑G'.unop).verts → W)
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
[PROOFSTEP]
exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
[GOAL]
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
[PROOFSTEP]
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
[GOAL]
case intro.intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
⊢ Nonempty (G →g F)
[PROOFSTEP]
refine' ⟨⟨fun v => _, _⟩⟩
[GOAL]
case intro.intro.refine'_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ W
[PROOFSTEP]
exact
  (u (Opposite.op (singletonFinsubgraph v))).toFun
    ⟨v, by
      unfold singletonFinsubgraph
      simp⟩
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts
[PROOFSTEP]
unfold singletonFinsubgraph
[GOAL]
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑(Opposite.op { val := SimpleGraph.singletonSubgraph G v, property := (_ : Set.Finite {v}) }).unop).verts
[PROOFSTEP]
simp
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
⊢ ∀ {a b : V},
    Adj G a b →
      Adj F
        ((fun v =>
            RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
              { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
          a)
        ((fun v =>
            RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
              { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
          b)
[PROOFSTEP]
intro v v' e
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    ((fun v =>
        RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
          { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
      v)
    ((fun v =>
        RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
          { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
      v')
[PROOFSTEP]
simp only
  /- The homomorphism for each edge's singleton subgraph agrees with those for its source and
          target vertices. -/
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj F
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v)))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun (u (Opposite.op (singletonFinsubgraph v')))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
rw [← hu hv, ← hu hv']
  -- porting note: was `apply Hom.map_adj`
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj F
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv (u (Opposite.op (finsubgraphOfAdj e))))
      { val := v, property := (_ : v ∈ (↑(Opposite.op (singletonFinsubgraph v)).unop).verts) })
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv' (u (Opposite.op (finsubgraphOfAdj e))))
      { val := v', property := (_ : v' ∈ (↑(Opposite.op (singletonFinsubgraph v')).unop).verts) })
[PROOFSTEP]
refine'
  Hom.map_adj (u (Opposite.op (finsubgraphOfAdj e)))
    _
      -- `v` and `v'` are definitionally adjacent in `finsubgraphOfAdj e`
[GOAL]
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ Adj (Subgraph.coe ↑(Opposite.op (finsubgraphOfAdj e)).unop)
    { val := v, property := (_ : v ∈ (↑(Opposite.op (finsubgraphOfAdj e)).unop).verts) }
    { val := v', property := (_ : v' ∈ (↑(Opposite.op (finsubgraphOfAdj e)).unop).verts) }
[PROOFSTEP]
simp [finsubgraphOfAdj]
