CrowellExactSequence.zcCompletedDifferentialModulePreStageMap_relation_iff_stage_mkQ_eq_zero
A pre-stage reduction is a finite relation exactly when its finite universal-module class is zero.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
universe uLean source · statement
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)