OAI/GroupTheory/PolycyclicRecognition/Geometry/FactorExponentialOverlap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common exponential coordinates on the intersection of the factors

  1. theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.factor_overlap_coordinates line 23

    Source documentation

    The recorded intersection theorem supplies a single tangent vector for both factor coordinates, using only injectivity of their actual inclusions.

    theorem factor_overlap_coordinates (n : F.N.carrier) (d : F.D.carrier)
    (he : F.inclusionN n = F.inclusionD d) :
    ∃ x : GroupLieAlgebra (𝓘(ℝ,E)) G, ∃ hx : x ∈ T.kernelIdeal, ∃ hy : x ∈ H,
      n = F.ExpN (F.N.equiv ⟨x,hx⟩) ∧ d = F.ExpD (F.D.equiv ⟨x,hy⟩) := by
…