Operations on split and threshold certificates

Transport preserves the supplied partition, rather than selecting a new one. A threshold certificate packages this partition with its nested-neighborhood proof.

def SimpleGraph.SplitPartition.mapIso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (P : G.SplitPartition) (f : G ≃g H) : H.SplitPartition

Relabel a split partition along an isomorphism.

Equations

• P.mapIso f = { clique := ⇑f.symm ⁻¹' P.clique, independent := ⇑f.symm ⁻¹' P.independent, isClique := ⋯, isIndepSet := ⋯, disjoint := ⋯, cover := ⋯ }

@[simp]

theorem SimpleGraph.SplitPartition.compl_clique {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) : P.compl.clique = P.independent

The clique part of a complemented partition is its original independent part.

@[simp]

theorem SimpleGraph.SplitPartition.compl_independent {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) : P.compl.independent = P.clique

The independent part of a complemented partition is its original clique part.

@[simp]

theorem SimpleGraph.SplitPartition.induce_clique {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (s : Set V) : (P.induce s).clique = Subtype.val ⁻¹' P.clique

Restricting a partition restricts its clique part by preimage.

@[simp]

theorem SimpleGraph.SplitPartition.induce_independent {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (s : Set V) : (P.induce s).independent = Subtype.val ⁻¹' P.independent

Restricting a partition restricts its independent part by preimage.

@[simp]

theorem SimpleGraph.SplitPartition.mem_mapIso_clique {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (P : G.SplitPartition) (f : G ≃g H) (v : W) : v ∈ (P.mapIso f).clique ↔ f.symm v ∈ P.clique

Membership in a relabelled clique is tested in the supplied original partition.

@[simp]

theorem SimpleGraph.SplitPartition.mem_mapIso_independent {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (P : G.SplitPartition) (f : G ≃g H) (v : W) : v ∈ (P.mapIso f).independent ↔ f.symm v ∈ P.independent

Membership in a relabelled independent part is tested in the original partition.

structure SimpleGraph.ThresholdPartition {V : Type u_1} (G : SimpleGraph V) extends G.SplitPartition : Type u_1

An explicit split partition with nested independent neighborhoods.

• clique : Set V
• independent : Set V
• isClique : G.IsClique self.clique
• isIndepSet : G.IsIndepSet self.independent
• disjoint : Disjoint self.clique self.independent
• cover : self.clique ∪ self.independent = Set.univ
• nested : self.HasNestedNeighborhoods

  Independent neighborhoods are comparable by inclusion.

theorem SimpleGraph.ThresholdPartition.isThreshold {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) : G.IsThreshold

A threshold partition certifies threshold membership.

def SimpleGraph.ThresholdPartition.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (P : G.ThresholdPartition) (f : W ↪ V) : (SimpleGraph.comap (⇑f) G).ThresholdPartition

Pull back the supplied threshold partition along an injective map.

Equations

• P.comap f = { toSplitPartition := P.comap f, nested := ⋯ }

def SimpleGraph.ThresholdPartition.induce {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) (s : Set V) : (SimpleGraph.induce s G).ThresholdPartition

Restrict the supplied threshold partition to an induced subgraph.

Equations

• P.induce s = P.comap (Function.Embedding.subtype s)

def SimpleGraph.ThresholdPartition.compl {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) : Gᶜ.ThresholdPartition

Complementation exchanges the parts and preserves nestedness.

Equations

• P.compl = { toSplitPartition := P.compl, nested := ⋯ }

def SimpleGraph.ThresholdPartition.mapIso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (P : G.ThresholdPartition) (f : G ≃g H) : H.ThresholdPartition

Relabel the supplied threshold partition.

Equations

• P.mapIso f = { toSplitPartition := P.mapIso f, nested := ⋯ }

@[simp]

theorem SimpleGraph.ThresholdPartition.induce_toSplitPartition {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) (s : Set V) : (P.induce s).toSplitPartition = P.induce s

Restriction uses the original split partition, not an existential replacement.

@[simp]

theorem SimpleGraph.ThresholdPartition.compl_toSplitPartition {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) : P.compl.toSplitPartition = P.compl

Complementation uses the original split partition with exchanged parts.

@[simp]

theorem SimpleGraph.ThresholdPartition.mapIso_toSplitPartition {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (P : G.ThresholdPartition) (f : G ≃g H) : (P.mapIso f).toSplitPartition = P.mapIso f

Relabelling uses the transported original split partition.

theorem SimpleGraph.isThreshold_iff_nonempty_thresholdPartition {V : Type u_1} {G : SimpleGraph V} : G.IsThreshold ↔ Nonempty G.ThresholdPartition

Threshold membership is equivalent to existence of an explicit threshold partition.

theorem SimpleGraph.IsThreshold.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (h : G.IsThreshold) (f : W ↪ V) : (SimpleGraph.comap (⇑f) G).IsThreshold

Threshold membership pulls back along an injective vertex map.