Finite convex geometries

This file proves the finite extreme-point and unique-basis consequences of anti-exchange used in the manuscript.

def QuotientSubmoduleEquidistribution.SetClosure.IsMinimalGenerator {E : Type u_1} (c : SetClosure E) (B C : Set E) : Prop

A generating set is inclusion-minimal when no one-point deletion still generates the same closed set. For closure operators this is equivalent to ordinary inclusion-minimality.

theorem QuotientSubmoduleEquidistribution.SetClosure.isMinimalGenerator_iff_no_proper_subset {E : Type u_1} {c : SetClosure E} {B C : Set E} : c.IsMinimalGenerator B C ↔ c B = C ∧ ∀ ⦃D : Set E⦄, D ⊂ B → c D ≠ C

One-point deletion minimality is equivalent to ordinary inclusion-minimality among generating sets.

theorem QuotientSubmoduleEquidistribution.SetClosure.not_mem_closure_union_of_finite {E : Type u_1} {c : SetClosure E} (hae : c.IsAntiExchange) {K Y : Set E} {b : E} (hK : c.IsClosed K) (hbK : b ∉ K) (hYfin : Y.Finite) (hY : Y ⊆ c (insert b K)) (hbY : b ∉ Y) : b ∉ c (K ∪ Y)

Anti-exchange can be iterated over a finite set: if all points of Y are available after adding b to a closed set K, then adjoining all of Y without b still cannot regenerate b.

theorem QuotientSubmoduleEquidistribution.SetClosure.exists_isMinimalGenerator {E : Type u_1} {c : SetClosure E} [Finite E] {C : Set E} (hC : c.IsClosed C) : ∃ (B : Set E), c.IsMinimalGenerator B C

Every closed set on a finite ground type has an inclusion-minimal generating set.

theorem QuotientSubmoduleEquidistribution.SetClosure.minimalGenerator_eq_extremePoints {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {B C : Set E} (hC : c.IsClosed C) (hB : c.IsMinimalGenerator B C) : B = c.extremePoints C

A one-point-minimal generator is the set of extreme points. This is the finite anti-exchange core of uniqueness of minimal generators.

theorem QuotientSubmoduleEquidistribution.SetClosure.closure_extremePoints {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {C : Set E} (hC : c.IsClosed C) : c (c.extremePoints C) = C

The extreme points form the unique minimal generating set of a closed set in a finite anti-exchange closure system.

theorem QuotientSubmoduleEquidistribution.SetClosure.extremePoints_nonempty {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) (hempty : c.IsClosed ∅) {C : Set E} (hC : c.IsClosed C) (hCne : C.Nonempty) : (c.extremePoints C).Nonempty

Every nonempty closed set in a finite convex geometry has an extreme point.

theorem QuotientSubmoduleEquidistribution.SetClosure.exists_extreme_not_mem_of_ssubset {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {C D : Set E} (hC : c.IsClosed C) (hD : c.IsClosed D) (hCD : C ⊂ D) : ∃ x ∈ c.extremePoints D, x ∉ C

A proper inclusion of finite closed sets admits a legal one-point deletion of the upper set which stays above the lower set.

theorem QuotientSubmoduleEquidistribution.SetClosure.exists_closed_sdiff_singleton_between {E : Type u_1} {c : SetClosure E} [Finite E] (hae : c.IsAntiExchange) {C D : Set E} (hC : c.IsClosed C) (hD : c.IsClosed D) (hCD : C ⊂ D) : ∃ x ∈ D \ C, c.IsClosed (D \ {x}) ∧ C ⊆ D \ {x}

Accessibility in interval form: a proper inclusion of finite closed sets can be shortened by deleting one extreme point from the upper set.