Transporting fusion models along homomorphisms

A homomorphism of interpretations sends every circuit constructing a problem to a circuit constructing the homomorphic image of that problem, with the same gates. Consequently a fusion model for the image problem yields a fusion model for the source problem: witnesses are unchanged and both predicates are read through the homomorphism. Atoms of the source circuit map to atoms of the image circuit, so covers transport with exactly the same operation cost.

This is the basic bridge for lower bounds that observe a circuit only after a restriction, a quotient, or another structure-preserving projection of its semantic values. Each homomorphism yields one transported lower bound; combining several images requires additional accounting.

def Algebraic.Fusion.Problem.map {U₁ : Type u_1} {U₂ : Type u_2} (problem : Problem U₁) (f : U₁ → U₂) : Problem U₂

Push a construction problem forward along a map of carriers.

Equations

• problem.map f = { inputCount := problem.inputCount, inputs := f ∘ problem.inputs, target := f problem.target }

@[simp]

theorem Algebraic.Fusion.Problem.map_inputCount {U₁ : Type u_1} {U₂ : Type u_2} (problem : Problem U₁) (f : U₁ → U₂) : (problem.map f).inputCount = problem.inputCount

@[simp]

theorem Algebraic.Fusion.Problem.map_inputs {U₁ : Type u_1} {U₂ : Type u_2} (problem : Problem U₁) (f : U₁ → U₂) (input : Fin problem.inputCount) : (problem.map f).inputs input = f (problem.inputs input)

@[simp]

theorem Algebraic.Fusion.Problem.map_target {U₁ : Type u_1} {U₂ : Type u_2} (problem : Problem U₁) (f : U₁ → U₂) : (problem.map f).target = f problem.target

theorem Algebraic.Fusion.Problem.Constructs.map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (h : Homomorphism i₁ i₂) {problem : Problem U₁} {circuit : Circuit σ problem.inputCount 1} (constructs : problem.Constructs circuit i₁) : (problem.map h.map).Constructs circuit i₂

A circuit constructing a problem constructs its homomorphic image.

def Algebraic.Fusion.Atom.map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} (atom : Atom σ U₁) (f : U₁ → U₂) : Atom σ U₂

Apply a carrier map to every argument of an atom.

Equations

• atom.map f = { op := atom.op, arguments := f ∘ atom.arguments }

@[simp]

theorem Algebraic.Fusion.Atom.map_op {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} (atom : Atom σ U₁) (f : U₁ → U₂) : (atom.map f).op = atom.op

@[simp]

theorem Algebraic.Fusion.Atom.map_arguments {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} (atom : Atom σ U₁) (f : U₁ → U₂) : (atom.map f).arguments = f ∘ atom.arguments

@[simp]

theorem Algebraic.Fusion.Atom.map_cost {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} (atom : Atom σ U₁) (f : U₁ → U₂) (operationCost : OperationCost σ) : (atom.map f).cost operationCost = atom.cost operationCost

theorem Algebraic.Fusion.Atom.listCost_map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} (atoms : List (Atom σ U₁)) (f : U₁ → U₂) (operationCost : OperationCost σ) : listCost (List.map (fun (atom : Atom σ U₁) => atom.map f) atoms) operationCost = listCost atoms operationCost

Mapping atoms preserves the total weight of a list.

theorem Algebraic.Fusion.Atom.map_result {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (h : Homomorphism i₁ i₂) (atom : Atom σ U₁) : (atom.map h.map).result i₂ = h.map (atom.result i₁)

The result of a mapped atom is the image of the original result.

@[reducible, inline]

abbrev Algebraic.Fusion.Model.comap {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (h : Homomorphism i₁ i₂) {operationCost : OperationCost σ} {problem : Problem U₁} (model : Model operationCost i₂ (problem.map h.map)) : Model operationCost i₁ problem

Pull a fusion model for the homomorphic image of a problem back to the source problem. Witnesses are unchanged; both predicates are evaluated on the image of a semantic value. The view is reducible so that the witness type of the pulled-back model is recognized as the witness type of the image model.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Atom.preservedBy_comap_iff {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) (model : Model operationCost i₂ (problem.map h.map)) (atom : Atom σ U₁) (witness : model.Witness) : atom.PreservedBy (Model.comap h model) witness ↔ (atom.map h.map).PreservedBy model witness

A witness preserves an atom in the pulled-back model exactly when it preserves the mapped atom in the image model.

def Algebraic.Fusion.Cover.map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) {model : Model operationCost i₂ (problem.map h.map)} (cover : Cover (Model.comap h model)) : Cover model

Push a cover of the pulled-back model forward to the image model.

Equations

• Algebraic.Fusion.Cover.map h cover = { atoms := List.map (fun (atom : Algebraic.Fusion.Atom σ U₁) => atom.map h.map) cover.atoms, isCover := ⋯ }

@[simp]

theorem Algebraic.Fusion.Cover.map_cost {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) {model : Model operationCost i₂ (problem.map h.map)} (cover : Cover (Model.comap h model)) : (map h cover).cost = cover.cost

Pushing a cover forward preserves its cost.

theorem Algebraic.Fusion.Model.coverComplexity_le_comap {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) (model : Model operationCost i₂ (problem.map h.map)) : model.coverComplexity ≤ (comap h model).coverComplexity

Cover complexity can only grow when a model is pulled back.

def Algebraic.Fusion.Framework.comap {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) {model : Model operationCost i₂ (problem.map h.map)} (framework : Framework model) : Framework (Model.comap h model)

A framework for the image model is a framework for the pulled-back model.

Equations

• Algebraic.Fusion.Framework.comap h framework = { bound := framework.bound, coverLowerBound := ⋯ }

@[simp]

theorem Algebraic.Fusion.Framework.comap_bound {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) {model : Model operationCost i₂ (problem.map h.map)} (framework : Framework model) : (comap h framework).bound = framework.bound

theorem Algebraic.Fusion.Framework.lowerBound_of_map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) {model : Model operationCost i₂ (problem.map h.map)} (framework : Framework model) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit i₁) : framework.bound ≤ circuit.cost operationCost

A fusion lower bound for the homomorphic image of a problem is a lower bound for every circuit constructing the source problem.

theorem Algebraic.Fusion.Model.coverComplexity_le_cost_of_map {σ : Signature} {U₁ : Type u_2} {U₂ : Type u_3} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} {operationCost : OperationCost σ} {problem : Problem U₁} (h : Homomorphism i₁ i₂) (model : Model operationCost i₂ (problem.map h.map)) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit i₁) : model.coverComplexity ≤ ↑(circuit.cost operationCost)

Cover complexity of an image model lower-bounds every source circuit.