CartanConeAction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The cone quotient action for the actual overlapping Cartan factors

theorem OAI.PolycyclicRecognition.CartanWordModel.mem_kernel_exp_iff line 32

Source documentation

In exponential coordinates the actual quotient kernel is exactly the given linear ideal.

theorem mem_kernel_exp_iff
    (I : LieIdeal ℝ (cartanRootIdeal H)) (π : N →* Q)
    (hker : (π.ker : Set N) = ExpN '' (eN '' (I : Set (cartanRootIdeal H))))
    (v : cartanRootIdeal H) : ExpN (eN v) ∈ π.ker ↔ v ∈ I := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.cone_kernel_adjoint_invariant line 46

Source documentation

The genuine adjoint group automorphism preserves the actual quotient kernel. No extra invariance hypothesis about the group is required.

theorem cone_kernel_adjoint_invariant
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (π : N →* Q)
    (hker : (π.ker : Set N) = ExpN '' (eN '' (M.coneWordIdeal C : Set (cartanRootIdeal H))))
    (h : H) (g : N) :
    M.adjointGroupAutomorphism T eN ExpN hExpN hbij dynkin h g ∈ π.ker ↔ g ∈ π.ker := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.cartan_factor_overlap_killed line 75

Source documentation

The already proved exact overlap of the actual factors is killed by the cone quotient, because its logarithm is in the zero weight space.

theorem cartan_factor_overlap_killed
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (hzero : (0 : H →ₗ[ℝ] ℝ) ∉ C)
    (π : F.N.carrier →* Q)
    (hπ : ∀ v : cartanRootIdeal H,
      π (F.ExpN (F.N.equiv v)) = 1 ↔ v ∈ M.coneWordIdeal C)
    (n : F.N.carrier) (d : F.D.carrier) (he : F.inclusionN n = F.inclusionD d) :
    π n = 1 := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.cartan_factor_cone_kernel_invariant line 101

Source documentation

Faithful exponential compatibility identifies the actual factor action with the adjoint automorphism, so its cone kernel invariance is derived.

theorem cartan_factor_cone_kernel_invariant
    (j : GroupLieAlgebra (𝓘(ℝ, EG)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
    (hρ : Function.Injective ρ)
    (hN : ∀ x : cartanRootIdeal H,
      ρ (F.inclusionN (F.ExpN (F.N.equiv x))) = algebraExpUnit (j x))
    (hD : ∀ h : H, ρ (F.inclusionD (F.ExpD (F.D.equiv h))) = algebraExpUnit (j h))
    (hNbij : Function.Bijective F.ExpN) (hDsurj : Function.Surjective F.ExpD)
    (dynkin : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (π : F.N.carrier →* Q)
    (hker : (π.ker : Set F.N.carrier) =
      F.ExpN '' (F.N.equiv '' (M.coneWordIdeal C : Set (cartanRootIdeal H))))
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput