Documentation Verification Report

AugmentationModule

📁 Source: ClassFieldTheory/Cohomology/AugmentationModule.lean

Statistics

Metric	Count
Definitions `aug`, `H1_iso`, `H1_iso'`, `aug_shortExactSequence`, `leftRegularToInd₁'`, `ofSubOfOne`, `ι`, `iso_ind₁'`	8
Theorems `H2_aug_isZero`, `aug_isShortExact`, `aug_isShortExact'`, `cohomology_aug_succ_iso`, `cohomology_aug_succ_iso'`, `exists_ofSubOfOne`, `leftRegularToInd₁'_comm`, `leftRegularToInd₁'_comm'`, `leftRegularToInd₁'_comp_leftRegularToInd₁'`, `leftRegularToInd₁'_comp_lsingle`, `leftReugularToInd₁'_single`, `ofSubOfOne_spec`, `sum_coeff_ι`, `tateCohomology_auc_succ_iso`, `ε_apply_ι`, `ε_comp_ι`, `trivialCohomology`, `trivialHomology`, `trivialTateCohomology`	19
Total	27

Rep

Definitions

Name	Category	Theorems
`aug` 📖	CompOp	15 math math: `split.sub_fst`, `aug.ε_apply_ι`, `split.apply_snd`, `aug.ε_comp_ι`, `split.ι_apply`, `aug.exists_ofSubOfOne`, `split.add_snd`, `aug.H2_aug_isZero`, `aug.ofSubOfOne_spec`, `aug.sum_coeff_ι`, `split.apply_fst`, `split.apply`, `split.ext_iff`, `split.add_fst`, `split.sub_snd`

Rep.aug

Definitions

Name	Category	Theorems
`H1_iso` 📖	CompOp	—
`H1_iso'` 📖	CompOp	—
`aug_shortExactSequence` 📖	CompOp	5 math math: `aug_isShortExact'`, `cohomology_aug_succ_iso'`, `tateCohomology_auc_succ_iso`, `aug_isShortExact`, `cohomology_aug_succ_iso`
`leftRegularToInd₁'` 📖	CompOp	5 math math: `leftRegularToInd₁'_comm`, `leftRegularToInd₁'_comp_lsingle`, `leftRegularToInd₁'_comm'`, `leftReugularToInd₁'_single`, `leftRegularToInd₁'_comp_leftRegularToInd₁'`
`ofSubOfOne` 📖	CompOp	1 math math: `ofSubOfOne_spec`
`ι` 📖	CompOp	7 math math: `ε_apply_ι`, `Rep.split.apply_snd`, `ε_comp_ι`, `exists_ofSubOfOne`, `ofSubOfOne_spec`, `sum_coeff_ι`, `Rep.split.apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`H2_aug_isZero` 📖	mathematical	—	`Rep.aug`	—	`groupCohomology.H1_isZero_of_trivial` `aug_isShortExact` `cohomology_aug_succ_iso`
`aug_isShortExact` 📖	mathematical	—	`aug_shortExactSequence`	—	`Rep.leftRegular.ε_epi`
`aug_isShortExact'` 📖	mathematical	—	`aug_shortExactSequence` `Rep.res` `Rep.instAdditiveRes`	—	`aug_isShortExact` `Rep.instAdditiveRes` `Rep.instIsRightAdjointRes` `Rep.instIsLeftAdjointRes`
`cohomology_aug_succ_iso` 📖	mathematical	—	`aug_shortExactSequence` `aug_isShortExact`	—	`aug_isShortExact` `Rep.isZero_of_trivialCohomology` `Rep.leftRegular.trivialCohomology`
`cohomology_aug_succ_iso'` 📖	mathematical	—	`aug_shortExactSequence` `Rep.res` `Rep.instAdditiveRes` `aug_isShortExact'`	—	`Rep.instAdditiveRes` `aug_isShortExact'` `Rep.isZero_of_injective` `Rep.leftRegular.trivialCohomology`
`exists_ofSubOfOne` 📖	mathematical	—	`Rep.aug` `ι` `Rep.leftRegular.of`	—	`Rep.exists_kernelι_eq` `Rep.leftRegular.ε_of`
`leftRegularToInd₁'_comm` 📖	mathematical	—	`leftRegularToInd₁'` `Representation.ind₁'`	—	`Rep.leftRegular.ρ_comp_lsingle` `leftRegularToInd₁'_comp_lsingle` `Representation.ind₁'_comp_lsingle`
`leftRegularToInd₁'_comm'` 📖	mathematical	—	`leftRegularToInd₁'` `Representation.ind₁'`	—	`Representation.ind₁'_comp_lsingle` `leftRegularToInd₁'_comp_lsingle` `Rep.leftRegular.ρ_comp_lsingle`
`leftRegularToInd₁'_comp_leftRegularToInd₁'` 📖	mathematical	—	`leftRegularToInd₁'`	—	`leftRegularToInd₁'_comp_lsingle`
`leftRegularToInd₁'_comp_lsingle` 📖	mathematical	—	`leftRegularToInd₁'`	—	`leftReugularToInd₁'_single`
`leftReugularToInd₁'_single` 📖	mathematical	—	`leftRegularToInd₁'`	—	—
`ofSubOfOne_spec` 📖	mathematical	—	`Rep.aug` `ι` `ofSubOfOne` `Rep.leftRegular.of`	—	`exists_ofSubOfOne`
`sum_coeff_ι` 📖	mathematical	—	`Rep.aug` `ι`	—	`ε_apply_ι` `Rep.leftRegular.ε_eq_sum`
`tateCohomology_auc_succ_iso` 📖	mathematical	—	`groupCohomology.tateCohomology` `aug_shortExactSequence` `groupCohomology.TateCohomology.δ` `aug_isShortExact`	—	`Rep.leftRegular.trivialTateCohomology` `TateCohomology.isIso_δ` `aug_isShortExact`
`ε_apply_ι` 📖	mathematical	—	`Rep.leftRegular.ε` `Rep.aug` `ι`	—	`ε_comp_ι`
`ε_comp_ι` 📖	mathematical	—	`Rep.aug` `ι` `Rep.leftRegular.ε`	—	—

Rep.leftRegular

Definitions

Name	Category	Theorems
`iso_ind₁'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trivialCohomology` 📖	mathematical	—	`Rep.TrivialCohomology`	—	`Rep.TrivialCohomology.of_iso` `Rep.trivialCohomology_ind₁'`
`trivialHomology` 📖	mathematical	—	`Rep.TrivialHomology`	—	`Rep.TrivialHomology.of_iso` `Rep.trivialHomology_ind₁'`
`trivialTateCohomology` 📖	mathematical	—	`Rep.TrivialTateCohomology`	—	`Rep.TrivialTateCohomology.of_iso` `Rep.trivialTateCohomology_ind₁'`

---

← Back to Index