Lifting Classifications Along the Transformation Taxonomy

SE.Persistence.Reference.Lift

A classification stated at family or kind granularity induces a classification over operator codes, by composing with operatorFamily and operatorKind from the Transformation theory.

Operators in the same family (kind) receive the same pattern by construction. This module does not choose a family-level classification; it only states how one is consumed at operator granularity.

This is the only module of the Persistence theory that imports the Transformation theory.

def SE.Persistence.Classification.liftFamily (c : Classification Transformation.TransformationFamily) : Classification Transformation.OperatorCode

The operator-level classification induced by a family-level one.

Equations

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

def SE.Persistence.Classification.liftKind (c : Classification Transformation.TransformationKind) : Classification Transformation.OperatorCode

The operator-level classification induced by a kind-level one.

Equations

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

theorem SE.Persistence.Classification.liftFamily_pattern_eq (c : Classification Transformation.TransformationFamily) {a b : Transformation.OperatorCode} (h : Transformation.operatorFamily a = Transformation.operatorFamily b) : c.liftFamily.pattern a = c.liftFamily.pattern b

Operators in the same family have the same pattern under a lifted classification.

theorem SE.Persistence.Classification.liftKind_pattern_eq (c : Classification Transformation.TransformationKind) {a b : Transformation.OperatorCode} (h : Transformation.operatorKind a = Transformation.operatorKind b) : c.liftKind.pattern a = c.liftKind.pattern b

Operators of the same kind have the same pattern under a lifted classification.

theorem SE.Persistence.Classification.liftFamily_coarse (c : Classification Transformation.TransformationFamily) (op : Transformation.OperatorCode) : c.liftFamily.coarse op = c.coarse (Transformation.operatorFamily op)

The coarse value at an operator is the coarse value at its family.

theorem SE.Persistence.Classification.liftKind_coarse (c : Classification Transformation.TransformationKind) (op : Transformation.OperatorCode) : c.liftKind.coarse op = c.coarse (Transformation.operatorKind op)

The coarse value at an operator is the coarse value at its kind.

theorem SE.Persistence.Classification.liftFamily_isPrs_iff (c : Classification Transformation.TransformationFamily) (op : Transformation.OperatorCode) : c.liftFamily.IsPrs op ↔ c.IsPrs (Transformation.operatorFamily op)

An operator is preserving exactly when its family is.

theorem SE.Persistence.Classification.liftKind_isPrs_iff (c : Classification Transformation.TransformationKind) (op : Transformation.OperatorCode) : c.liftKind.IsPrs op ↔ c.IsPrs (Transformation.operatorKind op)

An operator is preserving exactly when its kind is.

theorem SE.Persistence.Classification.liftFamily_wellFormed {c : Classification Transformation.TransformationFamily} (h : c.WellFormed) : c.liftFamily.WellFormed

Lifting along families preserves well-formedness.

theorem SE.Persistence.Classification.liftKind_wellFormed {c : Classification Transformation.TransformationKind} (h : c.WellFormed) : c.liftKind.WellFormed

Lifting along kinds preserves well-formedness.