OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicTriangularTopology.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The topology of the intrinsic triangular representation

The adjoint action recovers height continuously from the representation. On the height kernel the nilpotent exponential chart and unique triangular logarithm already recover the topology. Section coordinates combine them.

  1. theorem OAI.PolycyclicRecognition.intrinsic_triangular_representation_inducing line 26