Documentation

LeanPool.SmallUndecidableGroups.Host.ZIntersections

The subgroup intersections for the second compression HNN extension #

This file proves Proposition 3.8 of the paper inside the semantic Borisov group Gamma. Put Kc = ⟨t,c,k⟩. Then

The first equality is the base-intersection theorem for a restricted HNN extension. The second follows from Lemma B.5 of the paper, using the double-coset identity established in ZBaseIntersections.

source
@[reducible, inline]
abbrev Undecidability.HostZIntersections.FreeInput (datum : Thue.StandingDatum) :
BorisovCStage.RankFiveFree datum

The proved rank-five freeness witness for the concrete host model.

Equations
  • ⋯ = ⋯
Instances For
    source
    noncomputable def Undecidability.HostZIntersections.CTInGamma (datum : Thue.StandingDatum) :
    Subgroup (HostYStage.Gamma datum)

    The embedded subgroup ⟨t,c⟩ of Gamma.

    Equations
    Instances For
      source
      noncomputable def Undecidability.HostZIntersections.CInGamma (datum : Thue.StandingDatum) :
      Subgroup (HostYStage.Gamma datum)

      The embedded subgroup ⟨c⟩ of Gamma.

      Equations
      Instances For
        source
        noncomputable def Undecidability.HostZIntersections.Kc (datum : Thue.StandingDatum) :
        Subgroup (HostYStage.Gamma datum)

        K_c = ⟨t,c,k⟩ in the semantic Borisov group.

        Equations
        Instances For
          source
          noncomputable def Undecidability.HostZIntersections.CKInGamma (datum : Thue.StandingDatum) :
          Subgroup (HostYStage.Gamma datum)

          The subgroup ⟨c,k⟩ in the semantic Borisov group.

          Equations
          Instances For
            source
            theorem Undecidability.HostZIntersections.c_mem_CInGamma (datum : Thue.StandingDatum) :
            HostYStage.c datum ∈ CInGamma datum
            source
            theorem Undecidability.HostZIntersections.c_mem_CTInGamma (datum : Thue.StandingDatum) :
            HostYStage.c datum ∈ CTInGamma datum
            source
            theorem Undecidability.HostZIntersections.t_mem_CTInGamma (datum : Thue.StandingDatum) :
            HostYStage.t datum ∈ CTInGamma datum
            source
            theorem Undecidability.HostZIntersections.CTInGamma_le_Kc (datum : Thue.StandingDatum) :
            CTInGamma datum ≤ Kc datum
            source
            theorem Undecidability.HostZIntersections.c_mem_CKInGamma (datum : Thue.StandingDatum) :
            HostYStage.c datum ∈ CKInGamma datum
            source
            theorem Undecidability.HostZIntersections.k_mem_CKInGamma (datum : Thue.StandingDatum) :
            HostYStage.k datum ∈ CKInGamma datum
            source
            theorem Undecidability.HostZIntersections.CKInGamma_le_Kc (datum : Thue.StandingDatum) :
            CKInGamma datum ≤ Kc datum
            source
            theorem Undecidability.HostZIntersections.CTInGamma_le_HMinus (datum : Thue.StandingDatum) :
            CTInGamma datum ≤ HostYStage.HMinus datum
            source
            theorem Undecidability.HostZIntersections.Kc_inf_HMinus (datum : Thue.StandingDatum) :
            Kc datum ⊓ HostYStage.HMinus datum = CTInGamma datum

            The first equality of Proposition 3.8 of the paper: K_c ∩ H_y^- = ⟨t,c⟩.

            source
            theorem Undecidability.HostZIntersections.Kc_inf_HPlus (datum : Thue.StandingDatum) :
            Kc datum ⊓ HostYStage.HPlus datum = CKInGamma datum

            The second equality of Proposition 3.8 of the paper: K_c ∩ H_y^+ = ⟨c,k⟩.

            Compatibility with the first-stage attaching map #

            source
            noncomputable def Undecidability.HostZIntersections.CTInHMinus (datum : Thue.StandingDatum) :
            Subgroup ↥(HostYStage.HMinus datum)

            The copy of ⟨t,c⟩ as a subgroup of HMinus.

            Equations
            Instances For
              source
              noncomputable def Undecidability.HostZIntersections.CKInHPlus (datum : Thue.StandingDatum) :
              Subgroup ↥(HostYStage.HPlus datum)

              The copy of ⟨c,k⟩ as a subgroup of HPlus.

              Equations
              Instances For
                source
                theorem Undecidability.HostZIntersections.theta_mem_CT_iff_CK (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (a : ↥(HostYStage.HMinus datum)) :
                ↑a ∈ CTInGamma datum ↔ ↑(theta.equiv a) ∈ CKInGamma datum

                The isomorphism following Lemma 3.1 carries ⟨t,c⟩ exactly onto ⟨k,c⟩.

                source
                theorem Undecidability.HostZIntersections.theta_mem_Kc_iff (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (a : ↥(HostYStage.HMinus datum)) :
                ↑a ∈ Kc datum ↔ ↑(theta.equiv a) ∈ Kc datum

                Membership in K_c is preserved by the first-stage attaching isomorphism. This is the compatibility hypothesis needed to restrict the y-HNN extension to K_c.