SplittingModule

📁 Source: ClassFieldTheory/Cohomology/SplittingModule.lean

Statistics

Metric	Count
Definitions `split`, `FiniteClassFormation`, `H2Map₂`, `carrier`, `cocycle`, `reciprocityIso`, `representation`, `shortExactSequence`, `tateCohomologyIso`, `«term_↡_»`, `ι`, `π`, `τ`, `H2res`	14
Theorems `hypothesis₂`, `hypothesis₂'`, `isZero_H1`, `H2Map₂_H2π`, `H2Map₂_H2π_apply`, `H2Map₂_H2π_assoc`, `H2π_surjective`, `TateTheorem_lemma_1`, `TateTheorem_lemma_2`, `TateTheorem_lemma_3`, `TateTheorem_lemma_4`, `add_fst`, `add_snd`, `apply`, `apply_fst`, `apply_snd`, `cocycle_spec`, `ext`, `ext_iff`, `isIso_δ`, `isShortExact`, `res_isShortExact`, `splits`, `sub_fst`, `sub_snd`, `trivialCohomology`, `ι_apply`, `τ_property`	28
Total	42

Rep

Definitions

Name	Category	Theorems
`split` 📖	CompOp	14 math math: `split.sub_fst`, `split.TateTheorem_lemma_3`, `split.apply_snd`, `split.splits`, `split.TateTheorem_lemma_4`, `split.ι_apply`, `split.add_snd`, `split.τ_property`, `split.apply_fst`, `split.apply`, `split.TateTheorem_lemma_1`, `split.add_fst`, `split.trivialCohomology`, `split.sub_snd`

Rep.split

Definitions

Name	Category	Theorems
`FiniteClassFormation` 📖	CompData	—
`H2Map₂` 📖	CompOp	4 math math: `H2Map₂_H2π`, `H2Map₂_H2π_assoc`, `H2Map₂_H2π_apply`, `TateTheorem_lemma_1`
`carrier` 📖	CompOp	—
`cocycle` 📖	CompOp	5 math math: `apply_snd`, `splits`, `τ_property`, `apply`, `cocycle_spec`
`reciprocityIso` 📖	CompOp	—
`representation` 📖	CompOp	—
`shortExactSequence` 📖	CompOp	4 math math: `res_isShortExact`, `isIso_δ`, `isShortExact`, `TateTheorem_lemma_2`
`tateCohomologyIso` 📖	CompOp	—
`«term_↡_»` 📖	CompOp	—
`ι` 📖	CompOp	4 math math: `splits`, `ι_apply`, `τ_property`, `TateTheorem_lemma_1`
`π` 📖	CompOp	—
`τ` 📖	CompOp	1 math math: `τ_property`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`H2Map₂_H2π` 📖	mathematical	—	`H2Map₂`	—	—
`H2Map₂_H2π_apply` 📖	mathematical	—	`H2Map₂`	—	`H2Map₂_H2π`
`H2Map₂_H2π_assoc` 📖	mathematical	—	`H2Map₂`	—	`H2Map₂_H2π`
`H2π_surjective` 📖	—	—	—	—	—
`TateTheorem_lemma_1` 📖	mathematical	—	`H2Map₂` `Rep.res` `Rep.split` `ι`	—	`FiniteClassFormation.hypothesis₂` `cocycle_spec` `H2Map₂_H2π_apply` `splits`
`TateTheorem_lemma_2` 📖	mathematical	—	`shortExactSequence` `Rep.res` `Rep.instAdditiveRes` `res_isShortExact`	—	`Rep.instAdditiveRes` `res_isShortExact` `FiniteClassFormation.hypothesis₂'` `FiniteClassFormation.hypothesis₂` `TateTheorem_lemma_1`
`TateTheorem_lemma_3` 📖	mathematical	—	`Rep.res` `Rep.split`	—	`Rep.instAdditiveRes` `res_isShortExact` `TateTheorem_lemma_2` `FiniteClassFormation.isZero_H1`
`TateTheorem_lemma_4` 📖	mathematical	—	`Rep.res` `Rep.split`	—	`Rep.instAdditiveRes` `Rep.aug.aug_isShortExact'` `Rep.aug.cohomology_aug_succ_iso'` `groupCohomology.H1_isZero_of_trivial` `res_isShortExact` `TateTheorem_lemma_1`
`add_fst` 📖	mathematical	—	`Rep.aug` `Rep.split`	—	—
`add_snd` 📖	mathematical	—	`Rep.aug` `Rep.split`	—	—
`apply` 📖	mathematical	—	`Rep.split` `Rep.aug` `Rep.aug.ι` `cocycle`	—	—
`apply_fst` 📖	mathematical	—	`Rep.aug` `Rep.split`	—	—
`apply_snd` 📖	mathematical	—	`Rep.aug` `Rep.split` `Rep.aug.ι` `cocycle`	—	—
`cocycle_spec` 📖	mathematical	—	`cocycle`	—	`H2π_surjective`
`ext` 📖	—	`Rep.aug`	—	—	—
`ext_iff` 📖	mathematical	—	`Rep.aug`	—	`ext`
`isIso_δ` 📖	mathematical	—	`groupCohomology.tateCohomology` `shortExactSequence` `groupCohomology.TateCohomology.δ` `isShortExact`	—	`Rep.tateCohomology_of_trivialCohomology` `trivialCohomology` `TateCohomology.isIso_δ` `isShortExact`
`isShortExact` 📖	mathematical	—	`shortExactSequence`	—	—
`res_isShortExact` 📖	mathematical	—	`shortExactSequence` `Rep.res` `Rep.instAdditiveRes`	—	`Rep.instAdditiveRes` `Rep.shortExact_res` `isShortExact`
`splits` 📖	mathematical	—	`Rep.split` `ι` `cocycle`	—	`τ_property`
`sub_fst` 📖	mathematical	—	`Rep.aug` `Rep.split`	—	—
`sub_snd` 📖	mathematical	—	`Rep.aug` `Rep.split`	—	—
`trivialCohomology` 📖	mathematical	—	`Rep.TrivialCohomology` `Rep.split`	—	`groupCohomology.trivialCohomology_of_even_of_odd` `TateTheorem_lemma_4` `TateTheorem_lemma_3`
`ι_apply` 📖	mathematical	—	`Rep.split` `ι` `Rep.aug`	—	—
`τ_property` 📖	mathematical	—	`Rep.split` `τ` `ι` `cocycle`	—	`τ.eq_1` `apply` `ι_apply` `ext` `Rep.aug.ofSubOfOne_spec`

Rep.split.FiniteClassFormation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hypothesis₂` 📖	mathematical	—	`Rep.res` `groupCohomology.H2res`	—	—
`hypothesis₂'` 📖	mathematical	—	`Rep.res` `groupCohomology.H2res`	—	—
`isZero_H1` 📖	mathematical	—	`Rep.res`	—	—

groupCohomology

Definitions

Name	Category	Theorems
`H2res` 📖	CompOp	2 math math: `Rep.split.FiniteClassFormation.hypothesis₂'`, `Rep.split.FiniteClassFormation.hypothesis₂`

---

← Back to Index