Declarations
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard
DocumentationThe algebraic product \(I(\ker \psi)I(G)\) inside the algebraic standard source augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_generator_mem
DocumentationA generator \((n-1)s\) lies in the algebraic product \(I(\ker \psi)I(G)\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection
DocumentationProjection of the algebraic standard augmentation ideal to a finite augmentation stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_val
DocumentationThe value of the augmentation-ideal projection is the value of the corresponding finite-stage projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_zcCompletedGroupAlgebraStandardAugmentationIdealProjection
DocumentationThe standard augmentation-ideal projection is continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAStageAugmentationIdeal_identityBoundary_monoidAlgebraToIdentity
DocumentationOn a finite coefficient stage, the identity crossed-differential boundary is a left inverse to the additive lift from the finite augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_zero
DocumentationThe finite-stage augmentation-ideal projection is compatible with zero.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_add
DocumentationThe finite-stage augmentation-ideal projection is compatible with addition.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_smul
DocumentationThe finite-stage augmentation-ideal projection is compatible with scalar multiplication.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear
DocumentationThe finite-stage projection of the standard augmentation ideal, as a semilinear map over the completed group-algebra projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear_apply
DocumentationThe linear finite-stage projection of the standard completed augmentation ideal has the same value as its underlying projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_sub
DocumentationThe finite-stage augmentation-ideal projection is compatible with subtraction.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct
DocumentationThe product of all finite-stage projections of the standard completed augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct_apply
DocumentationEvaluating the product of standard augmentation-ideal projections at i returns the projection at i.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct_injective
DocumentationFinite-stage projections separate points of the standard completed augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_ext
DocumentationExtensionality for standard completed augmentation ideal elements by finite-stage projections.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_surjective
DocumentationEvery finite standard augmentation stage is hit by the completed standard augmentation ideal projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
DocumentationThe finite-stage product \(I(\ker)\,I(G/U)\) attached to the open-image quotient at a source stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAOpenImageKernelAugmentationIdealMulStageStandard_generator_mem
DocumentationA finite-stage product generator belongs to the finite-stage product submodule.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageKernelClass
DocumentationAn actual kernel element determines a class in the finite-stage open-image kernel.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageKernelClass_val
DocumentationThe open-image kernel class has the expected underlying subgroup, characterized by finite-stage Fox coordinate formulas.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdealProjection_kernel_generator_smul
DocumentationThe finite-stage augmentation-ideal projection is compatible with scalar multiplication.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKernelAugmentationIdealMulStandard_proj_mem_openImageStage
DocumentationProjecting an element of \(I(\ker\psi)I(G)\) to an open-image finite stage lands in the corresponding finite-stage kernel-augmentation product.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAOpenImageKernelAugmentationIdealMulStageStandard_mem_proj
DocumentationEvery element of the finite-stage open-image kernel-augmentation product is the projection of an element of the algebraic product \(I(\ker\psi)I(G)\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
DocumentationThe closed finite-stage hull of \(I(\ker \psi)I(G)\) inside the standard source augmentation ideal: an element belongs exactly when every finite projection belongs to the finite-stage open-image kernel product.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_le_closed
DocumentationThe algebraic product is contained in its finite-stage closed hull.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.isClosed_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
DocumentationThe finite-stage hull is closed in the standard source augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.closure_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_le_closed
DocumentationThe closure of the algebraic product is contained in the finite-stage closed hull.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed_le_closure
DocumentationThe finite-stage closed hull is contained in the closure of the algebraic product.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.closure_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_eq_closed
DocumentationThe closure of \(I(\ker \psi)I(G)\) is exactly the finite-stage kernel-product condition.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.isClosed_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_iff_eq_closed
DocumentationThe algebraic product is closed exactly when it already equals the finite-stage closed hull. This is the precise non-circular closedness frontier.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.KernelAugmentationIdealQuotient
DocumentationThe source-side augmentation quotient \(I\mathbb{Z}_C\llbracket G\rrbracket / I(\ker \psi) I\mathbb{Z}_C\llbracket G\rrbracket\), before descending scalars to \(\mathbb{Z}_C\llbracket H\rrbracket\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.KernelAugmentationIdealClosedQuotient
DocumentationThe closed source-side augmentation quotient, using the finite-stage closed hull of \(I(\ker \psi)I(G)\) as denominator.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.isQuotientMap_kernelAugmentationIdealClosedQuotient_mkQ
DocumentationThe quotient map to the closed source augmentation quotient is a quotient map.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kernelAugmentationIdealClosedQuotient_iff_comp_mkQ
DocumentationContinuity out of the closed source augmentation quotient can be tested after precomposing with the quotient map from the standard augmentation ideal.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.t1Space_kernelAugmentationIdealClosedQuotient
DocumentationThe closed source augmentation quotient is \(T_1\) for the quotient topology.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.isClosed_zero_kernelAugmentationIdealClosedQuotient
DocumentationThe zero class is closed in the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.KernelAugmentationIdealClosedStageQuotient
DocumentationThe finite-stage quotient of the source augmentation ideal by the open-image kernel product.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjection
DocumentationThe finite-stage coordinate of the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjection_mk
DocumentationThe stage projection of a closed kernel-augmentation quotient class is represented by the corresponding finite-stage projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kernelAugmentationIdealClosedQuotientStageProjection
DocumentationEach finite-stage coordinate of the closed source augmentation quotient is continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjectionProduct
DocumentationThe product of all finite-stage coordinates of the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjectionProduct_apply
DocumentationEvaluating the product projection of the closed kernel-augmentation quotient at i returns its stage projection at i.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kernelAugmentationIdealClosedQuotientStageProjectionProduct
DocumentationThe finite-stage coordinate product of the closed source augmentation quotient is continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjectionProduct_injective
DocumentationFinite-stage coordinates separate points in the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotientStageProjection_ext
DocumentationExtensionality for the closed source augmentation quotient by finite-stage coordinates.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedQuotient_topology_eq_induced_stageProjProduct
DocumentationThe quotient topology on the closed source augmentation quotient is exactly the topology induced by all finite closed-quotient coordinates.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageStageRingHom
DocumentationThe finite-stage source-to-open-image group-algebra map used to descend the source-stage action on the closed finite augmentation quotient to the matching target stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageStageRingHom_of
DocumentationThe open-image stage ring homomorphism sends generators according to the finite-stage Fox coordinate formula.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageStageRingHom_surjective
DocumentationThe finite-stage source-to-open-image group-algebra map is surjective.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageStageRingHom_ker_smul_mem
DocumentationSource-stage elements in the kernel of the open-image stage map multiply the finite augmentation stage into the finite kernel-product denominator.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotient_openImageStageRingHom_ker_smul_eq_zero
DocumentationSource-stage kernels act trivially on the closed finite augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotientTargetStageModule
DocumentationThe finite closed augmentation quotient as a module over the matching open-image target group-algebra stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotientTargetStageModule_map_smul
DocumentationThe stage quotient target module map is compatible with scalar multiplication.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedDifferentialModuleOpenImageIndex
DocumentationThe finite source quotient paired with the open-image target stage for a source group-algebra coordinate.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedDifferentialModuleOpenImageIndex_stageScalar
DocumentationThe open-image stage condition for the \(\mathbb{Z}_C\)-completed differential module is equivalent to the finite-stage coordinate condition.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotientBoundary
DocumentationThe finite source-boundary coordinate over the matching open-image target stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotientBoundaryLift
DocumentationThe finite-stage lift induced by the finite closed source-boundary coordinate.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelAugmentationIdealClosedStageQuotientBoundaryLift_single
DocumentationThe boundary lift lands in the finite-stage closed augmentation quotient by the Fox-differential kernel condition.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
DocumentationThe canonical quotient map from the algebraic kernel-product quotient to its closed finite-stage quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient_mk
DocumentationThe map from the algebraic kernel-product quotient to the closed quotient sends a representative to its closed quotient class.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKerAugQuotToClosedQuotient_inj_iff_eq_closed
DocumentationThe canonical map from the algebraic quotient \(I(G) / I(\ker \psi)I(G)\) to the closed finite-stage quotient is injective exactly when the algebraic product already equals its finite-stage closed hull.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.isClosed_zcCompletedGAKernelAugmentationIdealMulStandard_iff_toClosedQuotient_inj
DocumentationClosedness of \(I(\ker \psi)I(G)\) is equivalently the injectivity of the canonical map from the algebraic source augmentation quotient to the closed finite-stage quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
DocumentationThe source Fox boundary, valued in the source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
DocumentationThe source Fox boundary, valued in the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient_sourceBoundary
DocumentationThe map from the algebraic source augmentation quotient to the closed quotient sends source boundary classes to the corresponding closed source boundary classes.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_zcCompletedGASourceBoundaryToKerAugClosedQuot
DocumentationThe source Fox boundary into the closed source augmentation quotient is continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealQuotient_mk_generator_smul
DocumentationProducts \((n-1)s\) vanish in the source augmentation quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotient_groupLike_smul_eq_of_map_eq
DocumentationSource group-like actions with the same image under psi agree on the source augmentation quotient. This is the algebraic descent statement needed before a completed target scalar action can be installed.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
DocumentationThe additive endomorphism of the source augmentation quotient induced by any chosen lift of a target element.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_apply
DocumentationThe chosen-lift target group-like endomorphism acts by scalar multiplication with the completed group-like element of the selected source lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_eq_smul_of_map_eq
DocumentationThe chosen-lift target action agrees with scalar multiplication by any source lift of the same target element.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_one_apply
DocumentationThe chosen-lift target group-like endomorphism for the identity target element acts as the identity.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_mul_apply
DocumentationThe chosen-lift target group-like endomorphisms multiply pointwise on the quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective
DocumentationThe descended group-like target action on the source augmentation quotient, for a surjective \(\psi\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective_apply
DocumentationThe descended target group-like action for a surjective map acts through the selected source lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd
DocumentationCoefficients from \(\mathbb{Z}_C\) act on the source augmentation quotient through the source completed group algebra.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd_apply
DocumentationThe target coefficient endomorphism acts on the kernel-augmentation quotient by multiplication with the coefficient-map image of a.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffAction
DocumentationThe coefficient action of \(\mathbb{Z}_C\) on the source augmentation quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraCoeffMap_mul_groupLike_eq_groupLike_mul_coeffMap
DocumentationCoefficient elements are central with respect to group-like elements in \(\mathbb{Z}_C\llbracket G\rrbracket\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.kerAugQuotTargetGAActionOfSurj
DocumentationThe algebraic target group algebra \(\mathbb{Z}_C[H]\) acts on the source augmentation quotient. This is the dense algebraic part of the eventual completed \(\mathbb{Z}_C\llbracket H\rrbracket\) scalar action.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.kerAugQuotTargetGAActionOfSurj_of
DocumentationThe induced target group-algebra action evaluates on group-like elements by lifting through the chosen surjection.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
DocumentationThe descended algebraic Z_C[H]-module structure on the source augmentation quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.kerAugQuotTargetGAModuleOfSurj_smul
DocumentationThe target group-algebra module structure acts by the induced quotient action.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.kerAugQuotTargetGAModuleOfSurj_of_smul
DocumentationA group-like basis element acts on the target quotient module by the induced quotient action.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.kerAugQuotTargetGAModuleOfSurj_of_smul_eq_source_groupLike_smul
DocumentationThe algebraic target group-algebra action by \([h]\) agrees with source multiplication by any lift of \(h\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGASourceBoundaryToKerAugQuotTargetGACrossedHomOfSurjective
DocumentationThe source boundary is a crossed differential for the descended algebraic target group-algebra coefficients.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcAlgebraicDifferentialModuleToKernelAugmentationQuotientOfSurjective
DocumentationThe algebraic target-coefficient universal differential module maps to the source augmentation quotient by \(dg \mapsto\) \([g]-1\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcAlgebraicDifferentialModuleToKernelAugmentationQuotientOfSurjective_universal
DocumentationThe algebraic differential module maps universally to the kernel-augmentation quotient in the surjective case.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.mulStandard_mul_mem_of_mem_kernelAugIdealMul
DocumentationMultiplying an algebraic kernel-augmentation element by a standard augmentation element lands in the algebraic product \(I(\ker \psi)I(G)\). The remaining completed-target descent problem is exactly replacing the first hypothesis by membership in the completed map kernel.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
FoxDifferential.zcCompletedGAKernelAugmentationIdealMulStandard_mul_mem_closure_of_mem_ker_map
DocumentationUnder the finite-stage open-map kernel theorem, a completed-kernel scalar times a standard augmentation element lies in the closure of the algebraic product; no closedness hypothesis is assumed.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKernelAugmentationIdealMulStandard_mul_mem_closed_of_mem_ker_map
DocumentationIf \(k\) lies in the kernel of the completed group-algebra map, then \(k y\) lies in the finite-stage closed hull of \(I(\ker\psi)I(G)\) for every standard augmentation element \(y\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKernelAugmentationIdealMulStandard_kernelMulStandard_le_closed
DocumentationCompleted-kernel scalars send the standard source augmentation ideal into the finite-stage closed hull of \(I(\ker \psi)I(G)\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKernelAugmentationIdealMulStandard_kernelMulStandard_le_of_isClosed
DocumentationIf the algebraic product \(I(\ker \psi)I(G)\) is closed in the standard augmentation ideal, then completed-kernel scalars send standard augmentation elements into that product.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kernelMulStandard_le_of_toClosedQuotient_inj
DocumentationIf the canonical map from the algebraic source augmentation quotient to the closed finite-stage quotient is injective, then completed-kernel scalars multiply standard augmentation elements into the algebraic product \(I(\ker \psi)I(G)\). This descent step uses finite-stage closed membership and converts it back to algebraic membership through injectivity of the quotient comparison map.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKerAugQuot_ker_map_smul_eq_zero_of_kernelMulStandard_le
DocumentationIf every completed-kernel scalar sends the standard source augmentation ideal into \(I(\ker \psi)I(G)\), then the completed kernel acts trivially on the quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraTargetLiftOfSurjective
DocumentationConditional descent of the source action to a completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module. The extra hypothesis is exactly the missing kernel-product statement; it is kept explicit so that closure membership is not used as algebraic equality.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraMap_targetLiftOfSurjective
DocumentationFor a surjective presentation, the completed group-algebra map sends the chosen target lift of a back to a.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
DocumentationThe kernel-multiple containment hypothesis makes the source augmentation quotient a module over the target completed group algebra, using chosen lifts along the surjective presentation.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_closed_kernelMulStandard
DocumentationClosedness of the kernel-multiple submodule supplies the containment needed to descend the target completed-group-algebra module structure to the source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_ker_map_smul_eq_zero
DocumentationThe completed kernel acts trivially on the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kerAugClosedQuotTargetCompletedModuleOfSurj
DocumentationUnconditional descent of the source action to a completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module on the closed source augmentation quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kerAugClosedQuotTargetCompletedModuleOfSurj_map_smul
DocumentationThe closed quotient target module action is compatible with mapped scalars.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_zcCompletedGAKerAugClosedQuot_source_smul_const
DocumentationSource scalar multiplication on the closed source augmentation quotient is continuous in the source scalar, for a fixed quotient element.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kerAugClosedQuotTargetCompletedModuleOfSurj_smul_const
DocumentationDescended target scalar multiplication on the closed source augmentation quotient is continuous in the target scalar, for a fixed quotient element.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_source_smul
DocumentationSource scalar multiplication on the closed source augmentation quotient is jointly continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kerAugClosedQuotTargetCompletedModuleOfSurj_smul
DocumentationDescended target scalar multiplication on the closed source augmentation quotient is jointly continuous.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuousSMul_zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_source
DocumentationThe closed source augmentation quotient is a topological module for the source completed group algebra.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuousSMul_kerAugClosedQuotTargetCompletedModuleOfSurj
DocumentationThe descended target module structure on the closed source augmentation quotient is topological.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kerAugClosedQuotTargetCompletedModuleOfSurj_groupLike_smul
DocumentationGroup-like elements act on the closed quotient target module by the induced target action.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGASourceBoundaryToKerAugClosedQuotTargetCompletedCrossedHomOfSurjective
DocumentationThe source boundary to the closed source augmentation quotient is a crossed differential for the descended completed target scalars.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedGroupAlgebraOpenImageStageRingHom_projection_targetLift
DocumentationProjecting a chosen completed source lift of a target coefficient to a source stage and then passing to the open-image stage recovers the corresponding target finite-stage projection.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.kerAugIdealClosedQuotStageProj_liftLinear_eq_boundaryLift_preStageMap
DocumentationThe i-th closed augmentation quotient coordinate of the completed source-boundary lift factors through the corresponding open-image finite pre-stage.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_kernelAugmentationIdealClosedQuotientStageProjection_liftLinear
DocumentationEach finite closed-augmentation coordinate of the pre-quotient source-boundary lift is continuous for the finite-stage pre-module topology.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.continuous_crossedDiffModuleLiftLinear_sourceBoundaryToKerAugClosedQuot
DocumentationThe pre-quotient source-boundary lift to the closed source augmentation quotient is continuous for the finite-stage pre-module topology.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcSeparatedUniversalDifferentialSourceCompletedCrossedHom
DocumentationThe separated universal differential is also a crossed differential for source completed group-algebra scalars after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
DocumentationThe source-identity completed differential module maps to the separated module for \(\psi\) by \(dg \mapsto\) \(d_{\mathrm{sep}}\) g, with source scalars restricted through \(\mathbb{Z}_C\llbracket G\rrbracket\) \(\to\) \(\mathbb{Z}_C\llbracket H\rrbracket\).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcDiffModuleIdToZCSepDiffModule_universal
DocumentationThe comparison map from the identity differential module to the separated completed module sends the universal differential to the separated universal differential.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom_transition_mapStage
DocumentationThe finite source-identity coefficient map agrees with first projecting a completed source coefficient down to the source-identity stage and then applying the finite target map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageRingHom_projection_map
DocumentationCompleted source coefficients viewed at the identity-source stage agree with target finite projections after applying the completed group-algebra map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffModuleIdToZCSepDiffModule_stageProj
DocumentationFinite-stage projections of the identity-source lift to the separated \(\psi\)-module are computed by first projecting to the matching source-identity finite stage.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModuleStageBoundary_identitySourceStageToStage
DocumentationThe finite comparison from the source-identity stage to the \(\psi\)-stage commutes with the finite Fox boundary.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModuleIdentitySourceStageBoundary_stageProj
DocumentationApplying the finite identity boundary after the source-identity finite projection recovers the finite projection of the standard augmentation-valued completed Fox tail.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
omit [IsTopologicalGroup H] in
FoxDifferential.zcDiffModuleIdToZCSepDiffModule_eq_zero_of_zcToStandard_eq_zero
DocumentationThe identity-source lift to the separated \(\psi\)-module kills the kernel of the standard augmentation-valued completed Fox tail.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_zcToStdAugIdeal_naturalTopology
DocumentationThe standard-augmentation-valued completed Fox tail is continuous for the finite-stage natural topology on the completed differential module.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
omit [IsTopologicalGroup G] in
FoxDifferential.zcSeparatedCompletedDifferentialModule_source_kernel_groupLike_smul
DocumentationKernel group-like source scalars act trivially on the separated module after scalar restriction along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSeparatedCompletedDifferentialModule_source_map_smul
DocumentationSource scalar restriction on the separated module is exactly target scalar multiplication after applying the completed group-algebra map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSeparatedCompletedDifferentialModule_source_kernel_sub_one_smul
DocumentationElements of the source kernel augmentation ideal act trivially on the separated module after restricting scalars along the source map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffModuleIdToZCSepDiffModule_kernel_sub_one_smul
DocumentationThe identity-source lift to the separated module kills source kernel augmentation generators after scalar multiplication.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel
DocumentationA conditional source-standard-augmentation map to the separated module. The only remaining well-definedness input is that the identity Fox tail kernel is killed by the source-identity lift to the separated module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff
DocumentationThe source-standard-augmentation map to the separated module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
DocumentationThe conditional map out of the standard augmentation ideal recovers the canonical map from the completed differential module after composing with its quotient map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
DocumentationThe standard augmentation-ideal map recovers the canonical separated differential-module map after precomposition with the quotient map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_stageBoundary_stageProj
DocumentationFinite-stage boundary formula for the source-standard map into the separated module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_stageProj_eq_of_standardProj_eq
DocumentationThe finite-stage projection of the source-standard map depends only on the matching source-identity finite projection of the standard augmentation ideal.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_stdAugIdealToZCSepDiff_stageProj
DocumentationEach finite-stage coordinate of the source-standard map into the separated module is continuous. The coordinate factors through the matching finite standard augmentation projection.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_stdAugIdealToZCSepDiff_stageProjProduct
DocumentationThe product of all finite-stage coordinates of the source-standard map into the separated module is continuous.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_stdAugIdealToZCSepDiff
DocumentationThe source-standard map to the separated completed differential module is continuous for the finite-stage quotient topology.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel_boundary
DocumentationThe conditional augmentation-ideal map sends a group boundary to the separated universal differential of that group element.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_boundary
DocumentationThe augmentation-ideal map sends a group boundary to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel_kernel_generator_smul
DocumentationThe conditional source-standard map kills each algebraic kernel-product generator.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandard
DocumentationThe conditional source-standard map kills the algebraic product I(ker psi) I(G).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_kills_kernelMulStandard
DocumentationThe source-standard map kills the algebraic product I(ker psi) I(G).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
DocumentationIf the conditional source-standard map is continuous for the separated quotient topology, then killing the algebraic denominator implies that it kills the finite-stage closed denominator.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
DocumentationIf the source-standard map is continuous for the separated quotient topology, then it kills the closed finite-stage denominator.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed
DocumentationThe source-standard map kills the closed finite-stage denominator.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
DocumentationA conditional reverse map from the closed source augmentation quotient to the separated module. The remaining closed-denominator input is isolated as hclosed_kill.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill_boundary
DocumentationThe conditional map from the closed augmentation quotient sends the class of a boundary to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
DocumentationTarget-linear version of the conditional reverse map from the closed source augmentation quotient to the separated module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill_boundary
DocumentationThe target-linear conditional quotient map sends each boundary class to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap
DocumentationTarget-linear reverse map from the closed source augmentation quotient to the separated module, reducing the closed-denominator condition to continuity of the source-standard map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap_boundary
DocumentationUnder continuity of the conditional standard map, the target-linear quotient map sends a boundary class to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffOfClosedKill
DocumentationReverse map from the closed source augmentation quotient to the separated module, assuming only that the closed denominator is killed by the unconditional source-standard map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffOfClosedKill_boundary
DocumentationIf the closed denominator is killed, the resulting quotient map sends a boundary class to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_kerAugIdealQuotToZCSepDiffOfClosedKill
DocumentationThe reverse map from the closed source augmentation quotient to the separated module is continuous once the source-standard map is continuous.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfClosedKill
DocumentationTarget-linear reverse map from the closed source augmentation quotient to the separated module, assuming only that the closed denominator is killed by the unconditional source-standard map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfClosedKill_boundary
DocumentationThe target-linear map induced by annihilating the closed denominator has the expected value on boundary classes.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfContStdMap
DocumentationTarget-linear reverse map from the closed source augmentation quotient to the separated module, reducing the closed-denominator condition to continuity of the unconditional source-standard map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinearOfContStdMap_boundary
DocumentationContinuity of the standard map gives a target-linear quotient map with the expected value on boundary classes.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_kerAugIdealQuotToZCSepDiffLinearOfContStdMap
DocumentationThe target-linear reverse map obtained from a continuous source-standard map is continuous.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinear
DocumentationTarget-linear reverse map from the closed source augmentation quotient to the separated module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinear_boundary
DocumentationThe canonical target-linear reverse map sends each boundary class to the separated universal differential.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_kerAugIdealQuotToZCSepDiffLinear
DocumentationThe target-linear reverse map from the closed source augmentation quotient to the separated module is continuous.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
DocumentationThe completed universal differential module maps to the closed source augmentation quotient by \(dg \mapsto\) \([g]-1\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugClosedQuotOfSurj_universal
DocumentationThe closed augmentation-quotient map sends the universal differential to the class of the corresponding augmentation generator.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift
DocumentationIf the pre-quotient source-boundary lift to the closed augmentation quotient is continuous for the finite-stage pre-module topology, then it kills the finite-stage closed relation denominator. This is the descent criterion needed to factor the algebraic map through the separated completed differential module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift_of_surj
DocumentationVersion of zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift with nonemptiness and directedness of finite stages supplied by the continuous source map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjective
DocumentationUnder the explicit continuity hypothesis for the pre-quotient source-boundary lift, the closed source augmentation quotient receives the separated completed universal differential module.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
DocumentationPublic version of the closed-augmentation descent map with finite-stage nonemptiness and directedness supplied by the continuous source map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjective_universal
DocumentationThe separated differential module maps universally to the closed kernel-augmentation quotient in the surjective case.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_universal
DocumentationThe lifted map from the separated completed differential module to the closed augmentation-kernel quotient sends each separated universal differential to the corresponding boundary quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjective_comp_toSep
DocumentationThe separated closed-augmentation map is the factorization of the algebraic closed-augmentation map through \(A_{\psi}(C) \to A_{\psi}(C)_{\mathrm{sep}}\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_comp_toSep
DocumentationThe continuous-lift map to the closed kernel-augmentation quotient composes with separation as expected.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_zcSepDiffToKerAugClosedQuotOfSurjective
DocumentationThe descended forward map to the closed augmentation quotient is continuous once the pre-quotient source-boundary lift is continuous.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
DocumentationContinuity of the forward map when the finite-stage index data are supplied by the continuous source map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugClosedQuotOfSurj_surj
DocumentationThe map from the completed differential module to the closed augmentation quotient is surjective when finite-stage representatives can be lifted.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjective_surj
DocumentationThe separated closed-augmentation map is surjective under the same pre-quotient continuity hypothesis needed for the descent.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_surj
DocumentationThe continuous-lift map to the closed kernel-augmentation quotient is surjective.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
DocumentationThe separated completed universal differential module maps to the closed source augmentation quotient by \(dg \mapsto\) \([g]-1\). The pre-quotient lift continuity is supplied by the finite-stage factorization theorem.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuot_universal
DocumentationThe separated closed augmentation-quotient map sends the separated universal differential to the closed augmentation quotient class.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuot_comp_toSep
DocumentationThe unconditional separated closed-augmentation map factors the algebraic map through \(A_{\psi}(C) \to A_{\psi}(C)_{\mathrm{sep}}\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.continuous_zcSepDiffToKerAugClosedQuot
DocumentationThe separated closed-augmentation map is continuous, with the pre-quotient lift continuity provided by the finite-stage factorization theorem.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuot_surj
DocumentationThe separated map to the closed kernel-augmentation quotient is surjective.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinear_mk
DocumentationThe reverse map from the closed augmentation quotient to the separated differential module is evaluated on quotient classes by the constructed linear representative.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.kerAugIdealQuotToZCSepDiffLinear_comp_zcSepDiffToKerAugClosedQuot
DocumentationComposing the reverse closed-augmentation map with the forward separated map gives the identity.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffToKerAugClosedQuot_comp_kerAugIdealQuotToZCSepDiffLinear
DocumentationComposing the forward separated map with the reverse closed-augmentation map gives the identity.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffEquivKerAugClosedQuot_of_surj
DocumentationThe separated completed differential module is the closed source augmentation quotient for a surjective open continuous homomorphism.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffEquivKerAugClosedQuot_of_surj_apply
DocumentationThe Fox-coordinate equivalence is evaluated by the finite-stage coordinate formula in the completed differential complex.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcSepDiffEquivKerAugClosedQuot_of_surj_symm_apply
DocumentationThe inverse Fox-coordinate equivalence is evaluated by reconstructing the class from its completed coordinate data.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcApsiEquivKerAugClosedQuot_of_surj
DocumentationThe closed source augmentation quotient equivalence identifies \(A_{\psi}(C)\) over \(\mathbb{Z}_C\) with the separated completed differential module, rather than with the raw algebraic quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcApsiEquivKerAugClosedQuot_of_surj_apply
DocumentationThe Fox-coordinate equivalence is evaluated by the finite-stage coordinate formula in the completed differential complex.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcApsiEquivKerAugClosedQuot_of_surj_symm_apply
DocumentationThe inverse Fox-coordinate equivalence is evaluated by reconstructing the class from its completed coordinate data.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_map_smul
DocumentationFor a surjective target map, the completed target scalar action on the kernel-augmentation quotient is compatible with applying the induced algebra map.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_groupLike_smul
DocumentationIn the descended target module structure, the group-like element of \(\psi(g)\) acts in the same way as the source group-like element of \(g\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.sourceBoundaryToKerAugTargetCrossedHomOfSurjectiveOfKernelMulStandardLe
DocumentationUnder the explicit kernel-product hypothesis, the source boundary is a crossed differential for the descended completed target scalars.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le
DocumentationUnder the explicit kernel-product hypothesis, the completed universal differential module maps to the algebraic source augmentation quotient by \(dg \mapsto [g]-1\). The hypothesis is the condition needed for the algebraic quotient \(I(G) / I(\ker \psi)I(G)\) to carry the completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module structure.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le_universal
DocumentationUnder the kernel-product hypothesis, the algebraic source augmentation quotient map sends the universal differential to the class of \([g]-1\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le_surj
DocumentationThe algebraic map \(A_{\psi}(C) \to I(G) / I(\ker \psi)I(G)\) is onto once the algebraic quotient has the completed target scalar action supplied by the explicit kernel-product hypothesis.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le
DocumentationUnder the explicit kernel-product hypothesis, the natural map from the algebraic source augmentation quotient to the closed quotient is \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le_mk
DocumentationThe natural map from the algebraic source augmentation quotient to the closed quotient sends each algebraic quotient class to its closed quotient class.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcDiffToKerAugClosedQuotOfSurj_eq_toClosed_comp_quotient_of_kernelMulStandard_le
DocumentationThe algebraic quotient map followed by the natural closed-quotient map is the closed quotient map already constructed directly from \(A_{\psi}(C)\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModule_sourceKernelGroupLikeSubOne_smul_eq_zero
DocumentationSource kernel group-like differences act trivially on \(A_{\psi}(C)\) after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex
FoxDifferential.zcCompletedDifferentialModule_kernelAugmentationIdealMulStandard_smul_eq_zero
DocumentationThe algebraic product \(I(\ker \psi)I(G)\) acts trivially on \(A_{\psi}(C)\) after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
universe u
section KernelAugmentationQuotient
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
attribute [local implicit_reducible] zcCompletedDifferentialModuleIdentitySourceIndex