Documentation

Atlas.LieGroups.code.SL2Basics

source
@[reducible, inline]
abbrev M2 :
Type
Instances For
    source
    @[reducible, inline]
    abbrev M2C :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev SL2R :
      Type
      Instances For
        source
        noncomputable def sl2R :
        LieSubalgebra ℝ M2
        Instances For
          source
          def basisH :
          M2
          Instances For
            source
            def basisE :
            M2
            Instances For
              source
              def basisF :
              M2
              Instances For
                source
                noncomputable def sl2C :
                LieSubalgebra ℂ M2C
                Instances For
                  source
                  def basisH_C :
                  M2C
                  Instances For
                    source
                    def basisE_C :
                    M2C
                    Instances For
                      source
                      def basisF_C :
                      M2C
                      Instances For
                        source
                        theorem lie_H_E_C :
                        ⁅basisH_C, basisE_C⁆ = 2 • basisE_C
                        source
                        theorem lie_H_F_C :
                        ⁅basisH_C, basisF_C⁆ = -2 • basisF_C
                        source
                        theorem lie_E_F_C :
                        ⁅basisE_C, basisF_C⁆ = basisH_C
                        source
                        def SO2 :
                        Subgroup SL2R
                        Instances For
                          source
                          def IwasawaA :
                          Subgroup SL2R
                          Instances For
                            source
                            def IwasawaN :
                            Subgroup SL2R
                            Instances For
                              source
                              def lieAlgK :
                              Submodule ℝ M2
                              Instances For
                                source
                                def lieAlgP :
                                Submodule ℝ M2
                                Instances For
                                  source
                                  theorem finrank_sl2C :
                                  Module.finrank ℂ ↥sl2C = 3
                                  source
                                  theorem finrank_sl2R :
                                  Module.finrank ℝ ↥sl2R = 3
                                  source
                                  instance sl2C_finiteDimensional :
                                  FiniteDimensional ℂ ↥sl2C
                                  source
                                  instance sl2R_finiteDimensional :
                                  FiniteDimensional ℝ ↥sl2R
                                  source
                                  instance sl2C_free :
                                  Module.Free ℂ ↥sl2C
                                  source
                                  instance sl2R_free :
                                  Module.Free ℝ ↥sl2R
                                  source
                                  theorem basisH_C_mem_sl2C :
                                  basisH_C ∈ sl2C
                                  source
                                  theorem basisE_C_mem_sl2C :
                                  basisE_C ∈ sl2C
                                  source
                                  theorem basisF_C_mem_sl2C :
                                  basisF_C ∈ sl2C
                                  source
                                  def sl2H :
                                  ↥sl2C
                                  Instances For
                                    source
                                    def sl2E :
                                    ↥sl2C
                                    Instances For
                                      source
                                      def sl2F :
                                      ↥sl2C
                                      Instances For
                                        source
                                        theorem basisH_C_ne_zero :
                                        basisH_C ≠ 0
                                        source
                                        theorem sl2H_ne_zero :
                                        sl2H ≠ 0
                                        source
                                        theorem sl2_lie_EF :
                                        ⁅sl2E, sl2F⁆ = sl2H
                                        source
                                        theorem sl2_lie_HE :
                                        ⁅sl2H, sl2E⁆ = 2 • sl2E
                                        source
                                        theorem sl2_lie_HF :
                                        ⁅sl2H, sl2F⁆ = -(2 • sl2F)
                                        source
                                        def sl2_isSl2Triple :
                                        IsSl2Triple sl2H sl2E sl2F
                                        Instances For