Documentation

TauCeti.GroupTheory.TitsSystem.Comap

Pulling a Tits system back along a homomorphism #

Let (B, N) be a Tits system in G and write T = B ∩ N. If f : H →* G is a group homomorphism with G = f(H) T, that is, every element of G is f x * t for some x : H and some t ∈ B ∩ N, then the preimages f⁻¹(B) and f⁻¹(N) form a Tits system in H. Its Weyl group is canonically the Weyl group of (B, N), and its simple reflections are the preimages of the simple reflections of (B, N).

The main example is a normal subgroup H of G with G = H T, such as the special linear group inside the general linear group, where the diagonal torus supplies the missing determinants. The homomorphism need not be injective: pulling back along a surjection also gives a Tits system.

The key step is that Bruhat cells pull back to Bruhat cells: for w : H with f w ∈ N, the preimage of B f(w) B is the double coset f⁻¹(B) w f⁻¹(B) (TauCeti.TitsSystem.preimage_doubleCoset). This is where the hypothesis G = f(H) T enters, only through its consequence B ⊆ f(H) T: it lets the factors from B be replaced by factors from f⁻¹(B), with the leftover element of T moved past f w, which normalizes T.

Main declarations #

References #

source
theorem TauCeti.TitsSystem.preimage_doubleCoset {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] {f : H →* G} (hfB : ∀ b ∈ T.subgroupB, ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = b) {w : H} (hw : f w ∈ T.subgroupN) :
⇑f ⁻¹' DoubleCoset.doubleCoset (f w) ↑T.subgroupB ↑T.subgroupB = DoubleCoset.doubleCoset w ↑(Subgroup.comap f T.subgroupB) ↑(Subgroup.comap f T.subgroupB)

Bruhat cells pull back to Bruhat cells. If B ⊆ f(H) (B ∩ N), then for every w : H with f w ∈ N, the preimage of the double coset B f(w) B is the double coset f⁻¹(B) w f⁻¹(B).

source
def TauCeti.TitsSystem.comap {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
TitsSystem H

The pullback of a Tits system along a homomorphism f : H →* G with G = f(H) (B ∩ N): the subgroups f⁻¹(B) and f⁻¹(N) of H, with the simple reflections corresponding to those of (B, N) under the identification of Weyl groups TauCeti.TitsSystem.comapWeylGroupMulEquiv.

Instances For
    source
    @[simp]
    theorem TauCeti.TitsSystem.comap_subgroupB {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
    (T.comap f hf).subgroupB = Subgroup.comap f T.subgroupB

    The B subgroup of the pulled-back Tits system is the preimage of B.

    source
    @[simp]
    theorem TauCeti.TitsSystem.comap_subgroupN {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
    (T.comap f hf).subgroupN = Subgroup.comap f T.subgroupN

    The N subgroup of the pulled-back Tits system is the preimage of N.

    source
    noncomputable def TauCeti.TitsSystem.comapWeylGroupMulEquiv {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
    (T.comap f hf).WeylGroup ≃* T.WeylGroup

    The Weyl group of the pulled-back Tits system is the Weyl group of the original one: the class of n ∈ f⁻¹(N) corresponds to the class of f n.

    Instances For
      source
      @[simp]
      theorem TauCeti.TitsSystem.comapWeylGroupMulEquiv_mk {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) (n : ↥(T.comap f hf).subgroupN) :
      (T.comapWeylGroupMulEquiv f hf) ↑n = ↑⟨f ↑n, ⋯⟩

      The Weyl-group identification sends the class of n to the class of f n.

      source
      @[simp]
      theorem TauCeti.TitsSystem.comap_simple {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
      (T.comap f hf).simple = ⇑(T.comapWeylGroupMulEquiv f hf) ⁻¹' T.simple

      The simple reflections of the pulled-back Tits system are the preimages of the simple reflections of the original one under the identification of Weyl groups.

      source
      @[simp]
      theorem TauCeti.TitsSystem.comap_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) (w : (T.comap f hf).WeylGroup) :
      (T.comap f hf).bruhatCell w = ⇑f ⁻¹' T.bruhatCell ((T.comapWeylGroupMulEquiv f hf) w)

      A Weyl-indexed Bruhat cell of the pulled-back Tits system is the preimage of the cell indexed by the corresponding element of the original Weyl group.

      source
      theorem TauCeti.TitsSystem.normalCore_comap_subgroupB {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
      (T.comap f hf).subgroupB.normalCore = Subgroup.comap f T.subgroupB.normalCore

      The normal core ⋂ x f⁻¹(B) x⁻¹ of the pulled-back B is the preimage of the normal core ⋂ g B g⁻¹ of B: every g : G is f y * t with t ∈ B ∩ N, and t normalizes B.

      source
      @[simp]
      theorem TauCeti.TitsSystem.isIrreducible_comap_iff {G : Type u} [Group G] (T : TitsSystem G) {H : Type v} [Group H] (f : H →* G) (hf : ∀ (g : G), ∃ (x : H), ∃ t ∈ T.subgroupB ⊓ T.subgroupN, f x * t = g) :
      (T.comap f hf).IsIrreducible ↔ T.IsIrreducible

      A pulled-back Tits system is irreducible exactly when the original one is, since the two Weyl groups are identified together with their simple reflections.