ProCGroups.FoxDifferential.Completed.FiniteStage.RelationReflection

1 Theorem

This module records the elementary equivalence between membership in a finite-stage relation submodule and vanishing in its quotient.

import

ProCGroups.FoxDifferential.Completed.Continuous.Universal.FiniteStage

Imported by

Theorem CrowellExactSequence.zcCompletedDifferentialModulePreStageMap_relation_iff_stage_mkQ_eq_zero

theorem zcCompletedDifferentialModulePreStageMap_relation_iff_stage_mkQ_eq_zero
    {C : ProCGroups.FiniteGroupClass.{u}}
    {G H : Type u} [Group G] [TopologicalSpace G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {ψ : G →* H}
    {i : ZCCompletedDifferentialModuleIndex C ψ}
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :
    zcCompletedDifferentialModulePreStageMap C ψ i x ∈
        crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ i) ↔
      ((crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
        (zcCompletedDifferentialModulePreStageMap C ψ i x) = 0)

A pre-stage reduction is a finite relation exactly when its finite universal-module class is zero.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.RelationReflection

Declarations