Comparing Commitment Sets

SE.Persistence.Commitment.Compare

Two bodies of same-commitments P and Q generate two identity relations. This module says when one is contained in the other and, when they differ, that the difference is always pinned to a single commitment.

• Containment is checked on generators: Generated P is contained in Generated Q exactly when every pair of P is generated by Q.
• If it is not contained, some single pair of P is not generated by Q.

So a disagreement between two rules about who is the same as whom is never diffuse. Some specific asserted pair on one side accounts for it.

def SE.Persistence.GeneratedLE {C : Type} (P Q : C → C → Prop) : Prop

The identity generated by P is contained in the identity generated by Q.

Equations

• SE.Persistence.GeneratedLE P Q = ∀ (x y : C), SE.Persistence.Generated P x y → SE.Persistence.Generated Q x y

theorem SE.Persistence.generatedLE_iff {C : Type} {P Q : C → C → Prop} : GeneratedLE P Q ↔ ∀ (x y : C), P x y → Generated Q x y

Containment of generated identities is checked on generators.

theorem SE.Persistence.GeneratedLE.refl {C : Type} (P : C → C → Prop) : GeneratedLE P P

Containment is reflexive.

theorem SE.Persistence.GeneratedLE.trans {C : Type} {P Q R : C → C → Prop} (h1 : GeneratedLE P Q) (h2 : GeneratedLE Q R) : GeneratedLE P R

Containment is transitive.

theorem SE.Persistence.exists_generator_witness {C : Type} {P Q : C → C → Prop} (h : ¬GeneratedLE P Q) : ∃ (x : C), ∃ (y : C), P x y ∧ ¬Generated Q x y

If the identity generated by P is not contained in the one generated by Q, a single asserted pair of P is the cause: Q does not generate it.

theorem SE.Persistence.exists_generator_difference {C : Type} {P Q : C → C → Prop} (h : ¬(GeneratedLE P Q ∧ GeneratedLE Q P)) : ∃ (x : C), ∃ (y : C), P x y ∧ ¬Generated Q x y ∨ Q x y ∧ ¬Generated P x y

If P and Q generate different identity relations, a single asserted pair on one side accounts for the difference.