Modal Logic for scalar multiplication (SMul)

Any scalar multiplication operation • induces an accessibility relation where two elements are related if the latter is the result of applying a scalar multiplication to the former.

Properties of the operator translate to properties of the relation, for example a semigroup action on a commutative semigroup yields a relation with the Diamond property. This bridge allows for studying properties of the operation using modal logic.

def Relation.ofSMul (M : Type u_1) (α : Type u_2) [SMul M α] (x y : α) : Prop

The accessibility relation induced by a scalar multiplication operation: x is related to y when there exists m such that m • x = y.

Equations

• Relation.ofSMul M α x y = ∃ (m : M), m • x = y

instance Relation.instReflOfSMul {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] : Std.Refl (ofSMul M α)

The relation induced by a monoid action is reflexive.

instance Relation.instIsTransOfSMul {M : Type u_1} {α : Type u_2} [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α)

The relation induced by a semigroup action is transitive.

instance Relation.instSymmOfSMul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : Std.Symm (ofSMul G α)

The relation induced by a group action is symmetric.

instance Relation.instSerialOfSMulOfNonempty {M : Type u_1} {α : Type u_2} [SMul M α] [Nonempty M] : Serial (ofSMul M α)

The relation induced by an action of a nonempty type is serial.

instance Relation.instSMulCommClass_cslib {M : Type u_1} {α : Type u_2} [CommSemigroup M] [SemigroupAction M α] : SMulCommClass M M α

TODO: upstream this generalisation of Mathlib's smulCommClass_self, which applies only to monoids M.

theorem Relation.ofSMul_diamond {M : Type u_1} {α : Type u_2} [SMul M α] [SMulCommClass M M α] : Diamond (ofSMul M α)

The relation induced by an action commuting with itself has the diamond property.

theorem Relation.ofSMul_preserves_iff {M : Type u_1} {α : Type u_2} [SMul M α] {P : α → Prop} : Preserves (ofSMul M α) P ↔ ∀ (m : M) (x : α), P x → P (m • x)

Preservation by an action-induced relation is exactly closure under the action.

theorem Relation.ofSMul_preserves_mem {M : Type u_1} {α : Type u_2} {S : Type u_3} [SMul M α] [SetLike S α] [SMulMemClass S M α] (s : S) : Preserves (ofSMul M α) fun (x : α) => x ∈ s

Membership in a type closed under a scalar action is preserved by the relation induced by the action.

theorem Cslib.Logic.Modal.Proposition.ofSMul_diamond_denotation {M : Type u_1} {α : Type u_2} {β : Type u_3} [SMul M α] [Membership α β] (p : β) : denotation (Model.ofContainers (Relation.ofSMul M α)) (HasDiamond.diamond (atom p)) = {x : α | ∃ (m : M), m • x ∈ p}

Characterisation of the denotation of a ◇p under ofSMul.

theorem Cslib.Logic.Modal.Proposition.ofSMul_diamond_and_equiv {M : Type u_1} {α : Type u_2} {S : Type u_3} [CommSemigroup M] [SemigroupAction M α] [SetLike S α] [SMulMemClass S M α] (p q : S) : Congruence.r (Equiv.OfContainers (Relation.ofSMul M α)) (HasDiamond.diamond (HasAnd.and (atom p) (atom q))) (HasAnd.and (HasDiamond.diamond (atom p)) (HasDiamond.diamond (atom q)))

For SetLike objects closed under a commutative semigroup action, simultaneous reachability is equivalent to separate reachability.