Identity Equivalence

SE.Persistence.Relation.Equivalence

The identity relation ~_P of a classification: the equivalence relation generated by the steps of preserving transformations.

It depends on a classification only through its preserving set, so forgetting applicability (Classification.coarse) does not change it.

On the free dynamics it is characterized exactly: a transformation's private pair is identity-related precisely when the transformation preserves.

def SE.Persistence.Classification.identityRel {T C : Type} (c : Classification T) (d : Dynamics T C) : C → C → Prop

The identity relation ~_P.

Equations

• c.identityRel d = SE.Persistence.Generated (c.stepRel d)

theorem SE.Persistence.Classification.identityRel_equivalence {T C : Type} (c : Classification T) (d : Dynamics T C) : Equivalence (c.identityRel d)

~_P is an equivalence relation.

theorem SE.Persistence.Classification.survives_identityRel {T C : Type} {c : Classification T} {d : Dynamics T C} {x y : C} (h : c.Survives d x y) : c.identityRel d x y

Survival implies identity.

theorem SE.Persistence.Classification.identityRel_mono {T C : Type} {c c' : Classification T} (d : Dynamics T C) (h : ∀ (t : T), c.IsPrs t → c'.IsPrs t) {x y : C} (hg : c.identityRel d x y) : c'.identityRel d x y

A larger preserving set generates a larger identity relation.

theorem SE.Persistence.Classification.identityRel_eq_of_prs_iff {T C : Type} {c c' : Classification T} (d : Dynamics T C) (h : ∀ (t : T), c.IsPrs t ↔ c'.IsPrs t) : c.identityRel d = c'.identityRel d

Equal preserving sets give equal identity relations on every dynamics.

theorem SE.Persistence.Classification.identityRel_eq_of_coarse_eq {T C : Type} {c c' : Classification T} (d : Dynamics T C) (h : ∀ (t : T), c.coarse t = c'.coarse t) : c.identityRel d = c'.identityRel d

Classifications with the same coarse matrix have the same identity relation on every dynamics. Forgetting applicability does not change ~_P.

theorem SE.Persistence.Classification.identityRel_free_iff {T : Type} (c : Classification T) (t : T) : c.identityRel (freeDynamics T) (t, false) (t, true) ↔ c.IsPrs t

On the free dynamics, ~_P relates a transformation's private pair exactly when the transformation preserves.