OAI/GroupTheory/PolycyclicRecognition/Algebra/SplitKernelCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identifying an integrated kernel from local product coordinates

A normalized section turns a local product map into a product with the identity. The actual kernel is simply connected by retraction. A connected source with these local coordinates therefore maps homeomorphically onto that kernel, and its inclusion in the ambient group is closed.

  1. theorem OAI.PolycyclicRecognition.localHomeomorph_kernel_of_split_coordinates line 31
  2. theorem OAI.PolycyclicRecognition.closedEmbedding_kernel_of_split_coordinates line 62