Definition df-blockliftmap 38710

Description: Define the block lift map. Given a relation 𝑅 and a carrier/set 𝐴, we form the block relation (𝑅 ⋉ ^◡ E ) (i.e., "follow both 𝑅 and element"), restricted to 𝐴 (or, equivalently, "follow both 𝑅 and elements-of-A", cf. xrnres2 38677). Then map each domain element 𝑚 to its coset [𝑚] under that restricted block relation.

For 𝑚 in the domain, which requires (𝑚 ∈ 𝐴 ∧ 𝑚 ≠ ∅ ∧ [𝑚]𝑅 ≠ ∅) (cf. eldmxrncnvepres 38685), the fiber has the product form [𝑚](𝑅 ⋉ ^◡ E ) = ([𝑚]𝑅 × 𝑚), so the block relation lifts a block 𝑚 to the rectangular grid "external labels × internal members", see dfblockliftmap2 38712. Contrast: while the adjoined lift, via (𝑅 ∪ ^◡ E ), attaches neighbors and members in a single relation (see dfadjliftmap2 38708), the block lift labels each internal member by each external neighbor.

For the general case and a two-stage construction (first block lift, then adjoin membership), see the comments to df-adjliftmap 38706. For the equilibrium condition, see df-blockliftfix 38732. (Contributed by Peter Mazsa, 24-Jan-2026.) (Revised by Peter Mazsa, 22-Feb-2026.)

Assertion

Ref	Expression
df-blockliftmap	⊢ (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))

Detailed syntax breakdown of Definition df-blockliftmap

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cblockliftmap 38428	. 2 class (𝑅 BlockLiftMap 𝐴)
4		cep 5531	. . . . . 6 class E
5	4	ccnv 5631	. . . . 5 class ◡ E
6	5, 1	cres 5634	. . . 4 class (◡ E ↾ 𝐴)
7	2, 6	cxrn 38425	. . 3 class (𝑅 ⋉ (◡ E ↾ 𝐴))
8	7	cqmap 38426	. 2 class QMap (𝑅 ⋉ (◡ E ↾ 𝐴))
9	3, 8	wceq 1542	1 wff (𝑅 BlockLiftMap 𝐴) = QMap (𝑅 ⋉ (◡ E ↾ 𝐴))

This definition is referenced by:  dfblockliftmap  38711