Documentation

Linglib.Pragmatics.SocialMeaning.Dimension

This file characterizes the incompatibility relations that come from dimensions, and defines the dimensions on which hearers evaluate a speaker. Burnett's incompatibility relation on properties is any graph. It comes from dimensions, two properties being incompatible when they are distinct values of one, exactly when its complement, the compatibility graph, is complete multipartite, the dimensions being the parts; a persona, a maximal set of compatible properties, then takes one property of each part. The dimensions of social evaluation are competence and warmth, the two universal dimensions of social cognition of the Stereotype Content Model, and anti-solidarity, the factor of Beltrama, Solt and Burnett's ratings that loads apart from warmth, and their values are their two poles.

Main definitions #

SocialMeaning.dimensionalIncompatibility: the graph joining distinct values of one dimension.
Dimension: competence, warmth and anti-solidarity.
Pole: the six ends of the dimensions, with Pole.dimension and Pole.polarity.
Pole.opposite: the other end of a pole's dimension.

Main results #

SocialMeaning.isCompleteMultipartite_compl_iff: an incompatibility graph comes from dimensions exactly when its compatibility graph is complete multipartite.
SocialMeaning.mem_maximalIndepSets_iff_of_isCompleteMultipartite_compl: the personae are then the sets with exactly one property of each part.
Pole.eq_iff: a pole is determined by its dimension and polarity.
Pole.incompatible_adj_iff: two poles are incompatible when one is opposite the other.

References #

theorem SocialMeaning.mem_maximalIndepSets_iff_of_isCompleteMultipartite_compl {P : Type u} {G : SimpleGraph P} [Fintype P] [DecidableEq P] [DecidableRel G.Adj] (h : Gᶜ.IsCompleteMultipartite) {s : Finset P} :

s ∈ G.maximalIndepSets ↔ ∀ (p : P), {q ∈ s | q = p ∨ G.Adj q p}.card = 1

When the compatibility graph is complete multipartite, the personae are the sets with exactly one property of each class of mutually incompatible properties.

def SocialMeaning.dimensionalIncompatibility {P : Type u} {D : Type u_1} (dim : P → D) :

SimpleGraph P

The incompatibility of a family of dimensions joins two properties when they are distinct values of one dimension.

Equations

SocialMeaning.dimensionalIncompatibility dim = { Adj := fun (p q : P) => p ≠ q ∧ dim p = dim q, symm := ⋯, loopless := ⋯ }

Instances For

@[simp]

theorem SocialMeaning.dimensionalIncompatibility_adj {P : Type u} {D : Type u_1} {dim : P → D} {p q : P} :

(dimensionalIncompatibility dim).Adj p q ↔ p ≠ q ∧ dim p = dim q

@[instance_reducible]

instance SocialMeaning.instDecidableRelAdjDimensionalIncompatibilityOfDecidableEq {P : Type u} {D : Type u_1} {dim : P → D} [DecidableEq P] [DecidableEq D] :

DecidableRel (dimensionalIncompatibility dim).Adj

Equations

SocialMeaning.instDecidableRelAdjDimensionalIncompatibilityOfDecidableEq x✝¹ x✝ = { decide := decide (x✝¹ ≠ x✝) && decide (dim x✝¹ = dim x✝), reflects_decide := ⋯ }

theorem SocialMeaning.compl_dimensionalIncompatibility {P : Type u} {D : Type u_1} {dim : P → D} :

(dimensionalIncompatibility dim)ᶜ = SimpleGraph.comap dim ⊤

Two properties are compatible exactly when they are values of different dimensions.

theorem SocialMeaning.isCompleteMultipartite_compl_dimensionalIncompatibility {P : Type u} {D : Type u_1} {dim : P → D} :

(dimensionalIncompatibility dim)ᶜ.IsCompleteMultipartite

The compatibility graph of a family of dimensions is complete multipartite.

theorem SocialMeaning.isCompleteMultipartite_compl_iff {P : Type u} {G : SimpleGraph P} :

Gᶜ.IsCompleteMultipartite ↔ ∃ (D : Type u) (dim : P → D), dimensionalIncompatibility dim = G

An incompatibility graph comes from dimensions exactly when its compatibility graph is complete multipartite; the dimensions are then the parts.

theorem SocialMeaning.mem_maximalIndepSets_dimensionalIncompatibility_iff {P : Type u} {D : Type u_1} {dim : P → D} [Fintype P] [DecidableEq P] [DecidableEq D] {s : Finset P} :

s ∈ (dimensionalIncompatibility dim).maximalIndepSets ↔ ∀ (p : P), {x ∈ s | dim x = dim p}.card = 1

The personae of a family of dimensions are the sets with exactly one value of each dimension that has values.

inductive SocialMeaning.Dimension :

The dimensions of social evaluation are competence and warmth, and anti-solidarity, the factor on which pedantic and uptight load apart from the warmth scales.

competence : Dimension
warmth : Dimension
antiSolidarity : Dimension

Instances For

@[instance_reducible]

instance SocialMeaning.instDecidableEqDimension :

DecidableEq Dimension

Equations

SocialMeaning.instDecidableEqDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SocialMeaning.instFintypeDimension :

Fintype Dimension

Equations

SocialMeaning.instFintypeDimension = { elems := {SocialMeaning.Dimension.competence, SocialMeaning.Dimension.warmth, SocialMeaning.Dimension.antiSolidarity}, complete := ⋯ }

inductive SocialMeaning.Pole :

A pole is one end of a dimension of social evaluation.

competent : Pole
incompetent : Pole
warm : Pole
cold : Pole
solidary : Pole
antiSolidary : Pole

Instances For

@[instance_reducible]

instance SocialMeaning.instDecidableEqPole :

DecidableEq Pole

Equations

SocialMeaning.instDecidableEqPole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SocialMeaning.instFintypePole :

Fintype Pole

Equations

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

def SocialMeaning.Pole.polarity :

Pole → SignType

The polarity of a pole is positive at the end its dimension is named for, competent, warm and antisolidary, and negative at the other.

Equations

SocialMeaning.Pole.competent.polarity = 1
SocialMeaning.Pole.warm.polarity = 1
SocialMeaning.Pole.antiSolidary.polarity = 1
SocialMeaning.Pole.incompetent.polarity = -1
SocialMeaning.Pole.cold.polarity = -1
SocialMeaning.Pole.solidary.polarity = -1

Instances For

theorem SocialMeaning.Pole.eq_iff {p q : Pole} :

p = q ↔ p.dimension = q.dimension ∧ p.polarity = q.polarity

A pole is determined by its dimension and polarity.

def SocialMeaning.Pole.opposite :

The other end of a pole's dimension.

Equations

Instances For

@[simp]

theorem SocialMeaning.Pole.opposite_opposite (p : Pole) :

p.opposite.opposite = p

@[simp]

theorem SocialMeaning.Pole.dimension_opposite (p : Pole) :

p.opposite.dimension = p.dimension

@[simp]

theorem SocialMeaning.Pole.polarity_opposite (p : Pole) :

p.opposite.polarity = -p.polarity

def SocialMeaning.Pole.oppositeEquiv :

Equiv.Perm Pole

Pole.opposite as an involutive permutation.

Equations

SocialMeaning.Pole.oppositeEquiv = Function.Involutive.toPerm SocialMeaning.Pole.opposite SocialMeaning.Pole.opposite_opposite

Instances For

@[simp]

theorem SocialMeaning.Pole.oppositeEquiv_apply (p : Pole) :

oppositeEquiv p = p.opposite

@[simp]

theorem SocialMeaning.Pole.oppositeEquiv_symm :

Equiv.symm oppositeEquiv = oppositeEquiv

theorem SocialMeaning.Pole.dimension_surjective :

Function.Surjective dimension

theorem SocialMeaning.Pole.incompatible_adj_iff {p q : Pole} :

(dimensionalIncompatibility dimension).Adj p q ↔ q = p.opposite

Two poles are incompatible when one is opposite the other.

theorem SocialMeaning.Pole.mem_maximalIndepSets_iff (s : Finset Pole) :

s ∈ (dimensionalIncompatibility dimension).maximalIndepSets ↔ ∀ (d : Dimension), {x ∈ s | x.dimension = d}.card = 1

The personae are the sets with exactly one pole of each dimension.