Documentation

Mathlib.Combinatorics.Additive.Corner.Defs

Corners #

This file defines corners, namely triples of the form (x, y), (x, y + d), (x + d, y), and the property of being corner-free.

References #

theorem isCorner_iff {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) (x₁ : G) (y₁ : G) (x₂ : G) (y₂ : G) :
IsCorner A x₁ y₁ x₂ y₂ (x₁, y₁) A (x₁, y₂) A (x₂, y₁) A x₁ + y₂ = x₂ + y₁
structure IsCorner {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) (x₁ : G) (y₁ : G) (x₂ : G) (y₂ : G) :

A corner of a set A in an abelian group is a triple of points of the form (x, y), (x + d, y), (x, y + d). It is nontrivial if d ≠ 0.

Here we define it as triples (x₁, y₁), (x₂, y₁), (x₁, y₂) where x₁ + y₂ = x₂ + y₁ in order for the definition to make sense in commutative monoids, the motivating example being .

  • fst_fst_mem : (x₁, y₁) A
  • fst_snd_mem : (x₁, y₂) A
  • snd_fst_mem : (x₂, y₁) A
  • add_eq_add : x₁ + y₂ = x₂ + y₁
Instances For
    theorem IsCorner.fst_fst_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) :
    (x₁, y₁) A
    theorem IsCorner.fst_snd_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) :
    (x₁, y₂) A
    theorem IsCorner.snd_fst_mem {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) :
    (x₂, y₁) A
    theorem IsCorner.add_eq_add {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (self : IsCorner A x₁ y₁ x₂ y₂) :
    x₁ + y₂ = x₂ + y₁
    def IsCornerFree {G : Type u_1} [AddCommMonoid G] (A : Set (G × G)) :

    A corner-free set in an abelian group is a set containing no non-trivial corner.

    Equations
    Instances For
      theorem isCornerFree_iff {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {s : Set G} (hAs : A s ×ˢ s) :
      IsCornerFree A ∀ ⦃x₁ : G⦄, x₁ s∀ ⦃y₁ : G⦄, y₁ s∀ ⦃x₂ : G⦄, x₂ s∀ ⦃y₂ : G⦄, y₂ sIsCorner A x₁ y₁ x₂ y₂x₁ = x₂

      A convenient restatement of corner-freeness in terms of an ambient product set.

      theorem IsCorner.mono {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {B : Set (G × G)} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hAB : A B) (hA : IsCorner A x₁ y₁ x₂ y₂) :
      IsCorner B x₁ y₁ x₂ y₂
      theorem IsCornerFree.mono {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} {B : Set (G × G)} (hAB : A B) (hB : IsCornerFree B) :
      @[simp]
      theorem not_isCorner_empty {G : Type u_1} [AddCommMonoid G] {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} :
      ¬IsCorner x₁ y₁ x₂ y₂
      @[simp]
      theorem Set.Subsingleton.isCornerFree {G : Type u_1} [AddCommMonoid G] {A : Set (G × G)} (hA : A.Subsingleton) :
      theorem isCornerFree_singleton {G : Type u_1} [AddCommMonoid G] (x : G × G) :
      theorem IsCorner.image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanHom 2 s t f) (hAs : A s ×ˢ s) (hA : IsCorner A x₁ y₁ x₂ y₂) :
      IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

      Corners are preserved under 2-Freiman homomorphisms. -

      theorem IsCornerFree.of_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} (hf : IsAddFreimanHom 2 s t f) (hf' : Set.InjOn f s) (hAs : A s ×ˢ s) (hA : IsCornerFree (Prod.map f f '' A)) :

      Corners are preserved under 2-Freiman homomorphisms. -

      theorem isCorner_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanIso 2 s t f) (hAs : A s ×ˢ s) (hx₁ : x₁ s) (hy₁ : y₁ s) (hx₂ : x₂ s) (hy₂ : y₂ s) :
      IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) IsCorner A x₁ y₁ x₂ y₂
      theorem isCornerFree_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} (hf : IsAddFreimanIso 2 s t f) (hAs : A s ×ˢ s) :
      theorem IsCorner.of_image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} {x₁ : G} {y₁ : G} {x₂ : G} {y₂ : G} (hf : IsAddFreimanIso 2 s t f) (hAs : A s ×ˢ s) (hx₁ : x₁ s) (hy₁ : y₁ s) (hx₂ : x₂ s) (hy₂ : y₂ s) :
      IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)IsCorner A x₁ y₁ x₂ y₂

      Alias of the forward direction of isCorner_image.

      theorem IsCornerFree.image {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] {A : Set (G × G)} {s : Set G} {t : Set H} {f : GH} (hf : IsAddFreimanIso 2 s t f) (hAs : A s ×ˢ s) :

      Alias of the reverse direction of isCornerFree_image.