ArtinParabolicIntersections
DefinitionFor a Coxeter matrix M on a generating set S, the alternating word of length n starts with s and alternates s and t, with length zero giving the identity. The Artin group is the group presented by these generators and the relations equating the two alternating words of length M(s,t); its standard parabolic subgroup on T⊆S is generated by the generators indexed by T. A parabolic subgroup is any conjugate gPg⁻¹ of a standard parabolic subgroup, without a spherical-type restriction. For a metric space, the Gromov product is (x|y)ₒ=(d(o,x)+d(o,y)−d(x,y))/2. Gromov hyperbolicity means that some δ≥0 satisfies min{(x|y)ₒ,(y|z)ₒ}≤(x|z)ₒ+δ for every o,x,y,z. Being geodesic means that any x,y are the endpoints of an isometric image of the real interval [0,d(x,y)]. A sequence is a Gromov sequence at o when its pairwise Gromov products eventually exceed every real bound. An action is acylindrical if, for every ε>0, there are R∈ℝ and N∈ℕ such that, whenever d(x,y)≥R, the set of group elements moving both x and y by at most ε is finite and has cardinality at most N. Having three orbit limit points means that, from some basepoint o, three sequences of group elements produce Gromov sequences in its orbit, while the Gromov products between any two distinct sequences have a uniform upper bound over all pairs of indices. Acylindrical hyperbolicity is the defined proposition that the group admits an isometric acylindrical action with this three-sequence property on a geodesic Gromov-hyperbolic metric space. A subgroup P is weakly malnormal if P∩gPg⁻¹ is finite for some g. Finally, M is irreducible if every partition of S into two nonempty parts has a cross pair (s,t) with M(s,t)≠2.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ArtinParabolicIntersections.lean; bytes 16..3753
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
/-! Parabolic intersections, parabolic closure, and non-clique Artin-group dynamics. -/
namespace HarmonicArtin
universe u
variable {S : Type u}
def alternating (s t : S) : ℕ → FreeGroup S
| 0 => 1
| n + 1 => FreeGroup.of s * alternating t s n
def braidRelators (M : CoxeterMatrix S) : Set (FreeGroup S) :=
Set.range fun st : S × S =>
alternating st.1 st.2 (M st.1 st.2) *
(alternating st.2 st.1 (M st.1 st.2))⁻¹
abbrev Artin (M : CoxeterMatrix S) := PresentedGroup (braidRelators M)
def generator (M : CoxeterMatrix S) (s : S) : Artin M := PresentedGroup.of s
def artinParabolic (M : CoxeterMatrix S) (T : Set S) : Subgroup (Artin M) :=
Subgroup.closure (generator M '' T)
end HarmonicArtin
namespace HarmonicArtin.ParabolicIntersections
variable {G : Type*} [Group G]
/-- `g P g⁻¹`, with membership expressed without existential witnesses. -/
def conjugate (g : G) (P : Subgroup G) : Subgroup G :=
P.comap (MulAut.conj g⁻¹).toMonoidHom
variable {S : Type*} (M : CoxeterMatrix S)
/-- Conjugates of standard subgroups, with no spherical-type restriction. -/
def IsParabolic (P : Subgroup (Artin M)) : Prop :=
∃ (X : Set S) (g : Artin M), P = conjugate g (artinParabolic M X)
end HarmonicArtin.ParabolicIntersections
namespace HarmonicArtin.ParabolicIntersections
noncomputable def gromovProduct {X : Type} [MetricSpace X] (o x y : X) : ℝ :=
(dist o x + dist o y - dist x y)/2
def IsGromovHyperbolic (X : Type) [MetricSpace X] : Prop :=
∃ δ : ℝ, 0 ≤ δ ∧ ∀ o x y z : X,
min (gromovProduct o x y) (gromovProduct o y z) ≤ gromovProduct o x z + δ
def IsGeodesicMetric (X : Type) [MetricSpace X] : Prop :=
∀ x y : X, ∃ γ : Set.Icc (0 : ℝ) (dist x y) → X,
Isometry γ ∧ γ ⟨0,le_rfl,dist_nonneg⟩=x ∧ γ ⟨dist x y,dist_nonneg,le_rfl⟩=y
def IsGromovSequence {X : Type} [MetricSpace X] (o : X) (u : ℕ → X) : Prop :=
∀ R : ℝ, ∃ N : ℕ, ∀ m, N ≤ m → ∀ n, N ≤ n → R ≤ gromovProduct o (u m) (u n)
def IsAcylindrical (G X : Type) [Group G] [MetricSpace X] [MulAction G X] : Prop :=
∀ ε : ℝ, 0 < ε → ∃ R : ℝ, ∃ N : ℕ, ∀ x y : X, R ≤ dist x y →
{g : G | dist x (g • x) ≤ ε ∧ dist y (g • y) ≤ ε}.Finite ∧
{g : G | dist x (g • x) ≤ ε ∧ dist y (g • y) ≤ ε}.ncard ≤ N
def HasThreeOrbitLimitPoints (G X : Type) [Group G] [MetricSpace X] [MulAction G X] : Prop :=
∃ o : X, ∃ u : Fin 3 → ℕ → G,
(∀ i, IsGromovSequence o (fun n => u i n • o)) ∧
∀ i j, i ≠ j → ∃ B : ℝ, ∀ m n, gromovProduct o (u i m • o) (u j n • o) ≤ B
/-- An isometric non-elementary acylindrical action on a geodesic
Gromov-hyperbolic metric space. -/
def AcylindricallyHyperbolic (G : Type) [Group G] : Prop :=
∃ (X : Type) (metric : MetricSpace X) (action : MulAction G X),
@IsGeodesicMetric X metric ∧ @IsGromovHyperbolic X metric ∧
(∀ g : G, @Isometry X X metric.toPseudoMetricSpace.toPseudoEMetricSpace metric.toPseudoMetricSpace.toPseudoEMetricSpace
(fun x => @SMul.smul G X action.toSMul g x)) ∧
@IsAcylindrical G X _ metric action ∧ @HasThreeOrbitLimitPoints G X _ metric action
def WeaklyMalnormal {G : Type} [Group G] (P : Subgroup G) : Prop :=
∃ g : G, (↑(P ⊓ conjugate g P) : Set G).Finite
variable {S : Type} (M : CoxeterMatrix S)
/-- No nontrivial partition has every cross label equal to two. -/
def IsIrreducible : Prop :=
∀ Y : Set S, Y.Nonempty → Yᶜ.Nonempty → ∃ s ∈ Y, ∃ t ∉ Y, M s t ≠ 2
end HarmonicArtin.ParabolicIntersections
namespace HarmonicArtin.ParabolicIntersections
variable {S : Type} [Fintype S] [LinearOrder S] (M : CoxeterMatrix S)
end HarmonicArtin.ParabolicIntersections
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.