OAI/GroupTheory/PolycyclicRecognition/Algebra/ClosedEmbeddingSplitKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A closed kernel embedding gives a closed embedding over a split quotient

  1. def OAI.PolycyclicRecognition.splitKernelHom line 18

    Source documentation

    The homomorphism on the actual kernels.

    def splitKernelHom : (π.comp f).ker →* π.ker :=
…
  2. theorem OAI.PolycyclicRecognition.closedEmbedding_of_splitKernel line 27

    Source documentation

    Global section coordinates reduce closedness and the induced topology of a subgroup to those of its map on the kernel.

    theorem closedEmbedding_of_splitKernel
    (hk : Topology.IsClosedEmbedding (splitKernelHom f π)) :
    Topology.IsClosedEmbedding f := by
…

    Mentions: OAI.PolycyclicRecognition.splitKernelHom