Module

Surjective.lean

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Surjective

3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — differential module — map — surjective

The principal declarations in this module are:

primePowerCompletedGroupAlgebraMapLiftOfSurjective

A choice of a lift along the surjective completed group-algebra map \(\Lambda_G \to \Lambda_H\), independent of the displayed differential premodule topology.

primePowerCompletedGroupAlgebraMap_surjective

If \(\psi : G \to H\) is surjective, then the induced map of prime-power completed group algebras is surjective.

primePowerCompletedGroupAlgebraMap_liftOfSurjective

The chosen lift maps back to the target coefficient.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit

Imported by2

theorem

primePowerCompletedGroupAlgebraMap_surjective

L41 ↗

FoxDifferential.primePowerCompletedGroupAlgebraMap_surjective

Documentation

If \(\psi : G \to H\) is surjective, then the induced map of prime-power completed group algebras is surjective.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem primePowerCompletedGroupAlgebraMap_surjective
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ)

def

primePowerCompletedGroupAlgebraMapLiftOfSurjective

L137 ↗

FoxDifferential.primePowerCompletedGroupAlgebraMapLiftOfSurjective

Documentation

A choice of a lift along the surjective completed group-algebra map \(\Lambda_G \to \Lambda_H\), independent of the displayed differential premodule topology.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def primePowerCompletedGroupAlgebraMapLiftOfSurjective
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (a : PrimePowerCompletedGroupAlgebra ℓ H) :
    PrimePowerCompletedGroupAlgebra ℓ G

theorem

primePowerCompletedGroupAlgebraMap_liftOfSurjective

L147 ↗

FoxDifferential.primePowerCompletedGroupAlgebraMap_liftOfSurjective

Documentation

The chosen lift maps back to the target coefficient.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem primePowerCompletedGroupAlgebraMap_liftOfSurjective
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (a : PrimePowerCompletedGroupAlgebra ℓ H) :
    primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
        (primePowerCompletedGroupAlgebraMapLiftOfSurjective
          (ℓ := ℓ) (G := G) (H := H) ψ hψ a) = a

Module documentation

Fox differential: completed — differential module — map — surjective

Declarations

primePowerCompletedGroupAlgebraMap_surjective

primePowerCompletedGroupAlgebraMapLiftOfSurjective

primePowerCompletedGroupAlgebraMap_liftOfSurjective