Preimages as homomorphisms of set interpretations

Taking preimages under a map of ambient types commutes with intersection and union, so it is a homomorphism between the set interpretations of the AND/OR basis. The special case of the inclusion of a subset restricts every set to that subset: this is how a Boolean function is restricted to a subcube, and it lets a single circuit be observed through any chosen restriction.

def Algebraic.AndOr.preimageHomomorphism {Δ : Type u_1} {Γ : Type u_2} (f : Δ → Γ) : Homomorphism (setInterpretation Γ) (setInterpretation Δ)

Preimage under a map is a homomorphism of set interpretations.

Equations

• Algebraic.AndOr.preimageHomomorphism f = { map := fun (set : Set Γ) => f ⁻¹' set, homomorphic := ⋯ }

@[simp]

theorem Algebraic.AndOr.preimageHomomorphism_map {Δ : Type u_1} {Γ : Type u_2} (f : Δ → Γ) (set : Set Γ) : (preimageHomomorphism f).map set = f ⁻¹' set

@[reducible, inline]

abbrev Algebraic.AndOr.restrictHomomorphism {Γ : Type u_1} (subset : Set Γ) : Homomorphism (setInterpretation Γ) (setInterpretation ↑subset)

Restricting sets to a subset of the ambient type.

Equations

• Algebraic.AndOr.restrictHomomorphism subset = Algebraic.AndOr.preimageHomomorphism Subtype.val