Closure operators with anti-exchange

This file develops the abstract closure-theoretic layer used in paper/quotient_submodule_equidistribution/main.tex. The definitions do not assume that the ground type is finite; finiteness enters only in the later finite convex geometry results.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.SetClosure (E : Type u_1) : Type u_1

A closure operator on subsets of E.

def QuotientSubmoduleEquidistribution.SetClosure.IsFinitary {E : Type u_1} (c : SetClosure E) : Prop

Every point in a closure is already forced by a finite subset.

def QuotientSubmoduleEquidistribution.SetClosure.IsAntiExchange {E : Type u_1} (c : SetClosure E) : Prop

The anti-exchange axiom for a closure operator on subsets.

def QuotientSubmoduleEquidistribution.SetClosure.IsConvexGeometry {E : Type u_1} (c : SetClosure E) : Prop

The closure-theoretic axioms of a convex geometry.

Finiteness of the ground type is deliberately kept separate, so that the same API also applies to the finitary closures occurring for representation-infinite algebras.

def QuotientSubmoduleEquidistribution.SetClosure.extremePoints {E : Type u_1} (c : SetClosure E) (C : Set E) : Set E

The extreme points of C: the points not generated by the other points of C.

theorem QuotientSubmoduleEquidistribution.SetClosure.mem_extremePoints {E : Type u_1} {c : SetClosure E} {C : Set E} {x : E} : x ∈ c.extremePoints C ↔ x ∈ C ∧ x ∉ c (C \ {x})

theorem QuotientSubmoduleEquidistribution.SetClosure.isClosed_sdiff_singleton_of_not_mem_closure {E : Type u_1} {c : SetClosure E} {C : Set E} {x : E} (hC : c.IsClosed C) (hx : x ∉ c (C \ {x})) : c.IsClosed (C \ {x})

If deleting x from a closed set does not regenerate x, the deletion is closed.

theorem QuotientSubmoduleEquidistribution.SetClosure.mem_extremePoints_iff_isClosed_sdiff_singleton {E : Type u_1} {c : SetClosure E} {C : Set E} {x : E} (hC : c.IsClosed C) (hxC : x ∈ C) : x ∈ c.extremePoints C ↔ c.IsClosed (C \ {x})

For a point of a closed set, being extreme is equivalent to legal one-point deletion.

theorem QuotientSubmoduleEquidistribution.SetClosure.extremePoints_subset_of_closure_eq {E : Type u_1} {c : SetClosure E} {B C : Set E} (hBC : c B = C) : c.extremePoints C ⊆ B

Every generating set contains every extreme point.

theorem QuotientSubmoduleEquidistribution.SetClosure.isClosed_pointClosure_sdiff_singleton {E : Type u_1} {c : SetClosure E} (hfin : c.IsFinitary) (hae : c.IsAntiExchange) (hempty : c.IsClosed ∅) (x : E) : c.IsClosed (c {x} \ {x})

In a finitary anti-exchange closure with closed empty set, deleting the generating point from its point closure leaves a closed set.

This is the key step behind complete join-irreducibility of point closures in the manuscript.

theorem QuotientSubmoduleEquidistribution.SetClosure.pointClosure_injective {E : Type u_1} {c : SetClosure E} (hae : c.IsAntiExchange) (hempty : c.IsClosed ∅) : Function.Injective fun (x : E) => c {x}

Distinct points have distinct point closures in a convex geometry.