Tiles for tilings

This file defines some basic concepts related to individual tiles for tilings in a discrete context (with definitions in a continuous context to be developed separately but analogously).

Work in the field of tilings does not generally try to define or state things in any kind of maximal generality, so it is necessary to adapt definitions and statements from the literature to produce something that seems appropriately general for mathlib, covering a wide range of tiling-related concepts found in the literature. Nevertheless, further generalization may prove of use as this work is extended in future.

We work in the context of a space X acted on by a group G; the action is not required to be faithful, although typically it is. In a discrete context, tiles are expected to cover the space, or a subset of it being tiled when working with tilings not of the whole space, and the tiles are pairwise disjoint. In a continuous context, definitions in the literature vary; the tiles may be closed and cover the space with interiors required to be disjoint (as used by Grünbaum and Shephard or Goodman-Strauss), or they may be required to be measurable and to partition it up to null sets (as used by Greenfeld and Tao).

In general we are concerned not with a tiling in isolation but with tilings by some protoset of tiles; thus we make definitions in the context of such a protoset, where copies of the tiles in the tiling must be images of those tiles under the action of an element of the given group.

Where there are matching rules that say what combinations of tiles are considered as valid, these are provided as separate hypotheses where required. Tiles in a protoset are commonly considered in the literature to be marked in some way. When this is simply to distinguish two otherwise identical tiles, this is represented by the use of different indices in the protoset. When this is to give a tile fewer symmetries than it would otherwise have under the action of the given group, this is represented by the symmetries specified in the Prototile being less than its full stabilizer.

The group G is throughout here a multiplicative group. Additive groups are also used in the literature, typically when based on ℤ; to support the use of additive groups, to_additive could be used with the theory here.

Main definitions

• Prototile G X: A prototile in X as acted on by G, carrying the information of a subgroup of the stabilizer that says when two copies of the prototile are considered the same.

• Protoset G X ιₚ: An indexed family of prototiles.

• PlacedTile ps: An image of a tile in the protoset ps.

References

• Branko Grünbaum and G. C. Shephard, Tilings and Patterns
• Chaim Goodman-Strauss, Open Questions in Tiling
• Rachel Greenfeld and Terence Tao, A counterexample to the periodic tiling conjecture

structure DiscreteTiling.Prototile (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] : Type (max u_1 u_2)

A Prototile G X describes a tile in X, copies of which under elements of G may be used in tilings. Two copies related by an element of symmetries are considered the same; two copies not so related, even if they have the same points, are considered distinct.

• carrier : Set X

  The points in the prototile. Use the coercion to Set X, or ∈ on the Prototile, rather than using carrier directly. The coercion cannot use SetLike because it does not satisfy coe_injective.

• symmetries : Subgroup ↥(MulAction.stabilizer G ↑self)

  The group elements considered to be symmetries of the prototile.

theorem DiscreteTiling.Prototile.ext_iff {G : Type u_1} {X : Type u_2} {inst✝ : Group G} {inst✝¹ : MulAction G X} {x y : Prototile G X} : x = y ↔ ↑x = ↑y ∧ x.symmetries ≍ y.symmetries

theorem DiscreteTiling.Prototile.ext {G : Type u_1} {X : Type u_2} {inst✝ : Group G} {inst✝¹ : MulAction G X} {x y : Prototile G X} (carrier : ↑x = ↑y) (symmetries : x.symmetries ≍ y.symmetries) : x = y

instance DiscreteTiling.Prototile.instInhabited {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] : Inhabited (Prototile G X)

Equations

• DiscreteTiling.Prototile.instInhabited = { default := { carrier := ∅, symmetries := ⊥ } }

instance DiscreteTiling.Prototile.instCoeOutSet {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] : CoeOut (Prototile G X) (Set X)

Equations

• DiscreteTiling.Prototile.instCoeOutSet = { coe := DiscreteTiling.Prototile.carrier }

instance DiscreteTiling.Prototile.instMembership {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] : Membership X (Prototile G X)

Equations

• DiscreteTiling.Prototile.instMembership = { mem := fun (p : DiscreteTiling.Prototile G X) (x : X) => x ∈ ↑p }

theorem DiscreteTiling.Prototile.coe_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (c : Set X) (s : Subgroup ↥(MulAction.stabilizer G c)) : ↑{ carrier := c, symmetries := s } = c

@[simp]

theorem DiscreteTiling.Prototile.mem_coe {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {x : X} {p : Prototile G X} : x ∈ ↑p ↔ x ∈ p

structure DiscreteTiling.Protoset (G : Type u_1) (X : Type u_2) (ιₚ : Type u_3) [Group G] [MulAction G X] : Type (max (max u_1 u_2) u_3)

A Protoset G X ιₚ is an indexed family of Prototile G X. This is a separate definition rather than just using plain functions to facilitate defining associated API that can be used with dot notation.

• tiles : ιₚ → Prototile G X

  The tiles in the protoset. Use the coercion to a function rather than using tiles directly.

theorem DiscreteTiling.Protoset.ext {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {x y : Protoset G X ιₚ} (tiles : ↑x = ↑y) : x = y

theorem DiscreteTiling.Protoset.ext_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {x y : Protoset G X ιₚ} : x = y ↔ ↑x = ↑y

instance DiscreteTiling.Protoset.instInhabited {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] : Inhabited (Protoset G X ιₚ)

Equations

• DiscreteTiling.Protoset.instInhabited = { default := { tiles := fun (x : ιₚ) => default } }

instance DiscreteTiling.Protoset.instCoeFunForallPrototile {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] : CoeFun (Protoset G X ιₚ) fun (x : Protoset G X ιₚ) => ιₚ → Prototile G X

Equations

• DiscreteTiling.Protoset.instCoeFunForallPrototile = { coe := DiscreteTiling.Protoset.tiles }

theorem DiscreteTiling.Protoset.coe_mk {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] (t : ιₚ → Prototile G X) : ↑{ tiles := t } = t

@[simp]

theorem DiscreteTiling.Protoset.coe_inj {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps₁ ps₂ : Protoset G X ιₚ} : ↑ps₁ = ↑ps₂ ↔ ps₁ = ps₂

theorem DiscreteTiling.Protoset.coe_injective {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] : Function.Injective tiles

structure DiscreteTiling.PlacedTile {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] (ps : Protoset G X ιₚ) : Type (max u_1 u_3)

A PlacedTile ps is an image of a tile in the protoset p under an element of the group G. This is represented using a quotient so that images under group elements differing only by a symmetry of the tile are equal.

• index : ιₚ

  The index of the tile in the protoset.

• groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps self.index)).subtype (↑ps self.index).symmetries

  The group elements under which this tile is an image.

theorem DiscreteTiling.PlacedTile.ext {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {ps : Protoset G X ιₚ} {x y : PlacedTile ps} (index : x.index = y.index) (groupElts : x.groupElts ≍ y.groupElts) : x = y

theorem DiscreteTiling.PlacedTile.ext_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {ps : Protoset G X ιₚ} {x y : PlacedTile ps} : x = y ↔ x.index = y.index ∧ x.groupElts ≍ y.groupElts

instance DiscreteTiling.PlacedTile.instNonempty {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} [Nonempty ιₚ] : Nonempty (PlacedTile ps)

theorem DiscreteTiling.PlacedTile.induction_on {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {ppt : PlacedTile ps → Prop} (pt : PlacedTile ps) (h : ∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }) : ppt pt

An induction principle to deduce results for PlacedTile from those given an index and an element of G, used with induction pt using PlacedTile.induction_on.

theorem DiscreteTiling.PlacedTile.ext_iff_of_exists {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {pt₁ pt₂ : PlacedTile ps} : pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts

An alternative extensionality principle for PlacedTile that avoids HEq, using existence of a common group element.

theorem DiscreteTiling.PlacedTile.ext_iff_of_preimage {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {pt₁ pt₂ : PlacedTile ps} : pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ Quotient.mk (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹' {pt₁.groupElts} = Quotient.mk (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹' {pt₂.groupElts}

An alternative extensionality principle for PlacedTile that avoids HEq, using equality of quotient preimages.

def DiscreteTiling.PlacedTile.coeSet {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (pt : PlacedTile ps) : Set X

Coercion from a PlacedTile to a set of points. Use the coercion rather than using coeSet directly.

Equations

• ↑pt = Quotient.liftOn' pt.groupElts (fun (g : G) => g • ↑(↑ps pt.index)) ⋯

instance DiscreteTiling.PlacedTile.instCoeOutSet {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} : CoeOut (PlacedTile ps) (Set X)

Equations

• DiscreteTiling.PlacedTile.instCoeOutSet = { coe := DiscreteTiling.PlacedTile.coeSet }

instance DiscreteTiling.PlacedTile.instMembership {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} : Membership X (PlacedTile ps)

Equations

• DiscreteTiling.PlacedTile.instMembership = { mem := fun (p : DiscreteTiling.PlacedTile ps) (x : X) => x ∈ ↑p }

@[simp]

theorem DiscreteTiling.PlacedTile.mem_coe {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {x : X} {pt : PlacedTile ps} : x ∈ ↑pt ↔ x ∈ pt

theorem DiscreteTiling.PlacedTile.coe_mk_mk {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (i : ιₚ) (g : G) : ↑{ index := i, groupElts := ⟦g⟧ } = g • ↑(↑ps i)

theorem DiscreteTiling.PlacedTile.coe_mk_coe {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (i : ιₚ) (g : G) : ↑{ index := i, groupElts := ↑g } = g • ↑(↑ps i)

theorem DiscreteTiling.PlacedTile.coe_nonempty_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {pt : PlacedTile ps} : (↑pt).Nonempty ↔ (↑(↑ps pt.index)).Nonempty

@[simp]

theorem DiscreteTiling.PlacedTile.coe_mk_nonempty_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {i : ιₚ} (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries) : (↑{ index := i, groupElts := g }).Nonempty ↔ (↑(↑ps i)).Nonempty

theorem DiscreteTiling.PlacedTile.coe_finite_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {pt : PlacedTile ps} : (↑pt).Finite ↔ (↑(↑ps pt.index)).Finite

@[simp]

theorem DiscreteTiling.PlacedTile.coe_mk_finite_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {i : ιₚ} (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries) : (↑{ index := i, groupElts := g }).Finite ↔ (↑(↑ps i)).Finite

instance DiscreteTiling.PlacedTile.instSMul {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} : SMul G (PlacedTile ps)

Equations

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

@[simp]

theorem DiscreteTiling.PlacedTile.smul_mk_mk {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (g h : G) (i : ιₚ) : g • { index := i, groupElts := ⟦h⟧ } = { index := i, groupElts := ↑(g * h) }

@[simp]

theorem DiscreteTiling.PlacedTile.smul_mk_coe {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (g h : G) (i : ιₚ) : g • { index := i, groupElts := ↑h } = { index := i, groupElts := ↑(g * h) }

@[simp]

theorem DiscreteTiling.PlacedTile.smul_index {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (g : G) (pt : PlacedTile ps) : (g • pt).index = pt.index

@[simp]

theorem DiscreteTiling.PlacedTile.coe_smul {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (g : G) (pt : PlacedTile ps) : ↑(g • pt) = g • ↑pt

instance DiscreteTiling.PlacedTile.instMulAction {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} : MulAction G (PlacedTile ps)

Equations

• DiscreteTiling.PlacedTile.instMulAction = { toSMul := inferInstance, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem DiscreteTiling.PlacedTile.smul_mem_smul_iff {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} (g : G) {x : X} {pt : PlacedTile ps} : g • x ∈ g • pt ↔ x ∈ pt

theorem DiscreteTiling.PlacedTile.mem_smul_iff_smul_inv_mem {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {g : G} {x : X} {pt : PlacedTile ps} : x ∈ g • pt ↔ g⁻¹ • x ∈ pt

theorem DiscreteTiling.PlacedTile.mem_inv_smul_iff_smul_mem {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : Protoset G X ιₚ} {g : G} {x : X} {pt : PlacedTile ps} : x ∈ g⁻¹ • pt ↔ g • x ∈ pt