OAI/GroupTheory/PolycyclicRecognition/Geometry/FaithfulDifferential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A faithful group representation has faithful differential

If two tangent vectors have the same image, their represented one-parameter subgroups agree. Faithfulness of the representation and uniqueness of the tangent vector then identify the two vectors. No immersion theorem or global injectivity of the Lie exponential is required.

  1. theorem OAI.PolycyclicRecognition.injective_algebra_differential line 23