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 #

source
πŸ”Ά coverage
structure IsCorner {G : Type u_1} [AddCommMonoid G] (A : Set (G Γ— G)) (x₁ y₁ xβ‚‚ yβ‚‚ : G) :
Prop

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
    source
    πŸ“ coverage
    theorem isCorner_iff {G : Type u_1} [AddCommMonoid G] (A : Set (G Γ— G)) (x₁ y₁ xβ‚‚ yβ‚‚ : G) :
    IsCorner A x₁ y₁ xβ‚‚ yβ‚‚ ↔ (x₁, y₁) ∈ A ∧ (x₁, yβ‚‚) ∈ A ∧ (xβ‚‚, y₁) ∈ A ∧ x₁ + yβ‚‚ = xβ‚‚ + y₁
    source
    πŸ”Ή coverage
    def IsCornerFree {G : Type u_1} [AddCommMonoid G] (A : Set (G Γ— G)) :
    Prop

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

    Equations
      Instances For
        source
        πŸ“ coverage
        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β‚‚ ∈ s β†’ IsCorner A x₁ y₁ xβ‚‚ yβ‚‚ β†’ x₁ = xβ‚‚

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

        source
        theorem IsCorner.mono {G : Type u_1} [AddCommMonoid G] {A B : Set (G Γ— G)} {x₁ y₁ xβ‚‚ yβ‚‚ : G} (hAB : A βŠ† B) (hA : IsCorner A x₁ y₁ xβ‚‚ yβ‚‚) :
        IsCorner B x₁ y₁ xβ‚‚ yβ‚‚
        source
        theorem IsCornerFree.mono {G : Type u_1} [AddCommMonoid G] {A B : Set (G Γ— G)} (hAB : A βŠ† B) (hB : IsCornerFree B) :
        IsCornerFree A
        source
        πŸ“ coverage
        @[simp]
        theorem not_isCorner_empty {G : Type u_1} [AddCommMonoid G] {x₁ y₁ xβ‚‚ yβ‚‚ : G} :
        Β¬IsCorner βˆ… x₁ y₁ xβ‚‚ yβ‚‚
        source
        πŸ“ coverage
        @[simp]
        theorem Set.Subsingleton.isCornerFree {G : Type u_1} [AddCommMonoid G] {A : Set (G Γ— G)} (hA : A.Subsingleton) :
        IsCornerFree A
        source
        πŸ“ coverage
        theorem isCornerFree_empty {G : Type u_1} [AddCommMonoid G] :
        IsCornerFree βˆ…
        source
        πŸ“ coverage
        theorem isCornerFree_singleton {G : Type u_1} [AddCommMonoid G] (x : G Γ— G) :
        IsCornerFree {x}
        source
        πŸ“ coverage
        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 : G β†’ H} {x₁ y₁ xβ‚‚ 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.

        source
        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 : G β†’ H} (hf : IsAddFreimanHom 2 s t f) (hf' : Set.InjOn f s) (hAs : A βŠ† s Γ—Λ’ s) (hA : IsCornerFree (Prod.map f f '' A)) :
        IsCornerFree A

        Corners are preserved under 2-Freiman homomorphisms.

        source
        πŸ“ coverage
        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 : G β†’ H} {x₁ y₁ xβ‚‚ 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β‚‚
        source
        πŸ“ coverage
        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 : G β†’ H} (hf : IsAddFreimanIso 2 s t f) (hAs : A βŠ† s Γ—Λ’ s) :
        IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
        source
        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 : G β†’ H} {x₁ y₁ xβ‚‚ 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.

        source
        πŸ“ coverage
        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 : G β†’ H} (hf : IsAddFreimanIso 2 s t f) (hAs : A βŠ† s Γ—Λ’ s) :
        IsCornerFree A β†’ IsCornerFree (Prod.map f f '' A)

        Alias of the reverse direction of isCornerFree_image.