Inflation

📁 Source: ClassFieldTheory/Cohomology/Functors/Inflation.lean

Statistics

Metric	Count
Definitions quotientToInvariantsFunctor', res_quotientToInvariantsFunctor'_ι, «term_↑_», cochain_infl, infl	5
Theorems quotientKerEquivOfSurjective_symm_apply, instPreservesZeroMorphismsQuotientToInvariantsFunctor', quotientToInvariantsFunctor'_obj_V, quotientToInvariantsFunctor'_obj_ρ, quotientToInvariantsFunctor'_obj_ρ_apply, quotientToInvariantsFunctor'_obj_ρ_apply₂, res_quotientToInvariantsFunctor'_ι_hom_hom_apply, infl_δ_naturality	8
Total	13

Rep

Definitions

Name	Category	Theorems
quotientToInvariantsFunctor' 📖	CompOp	10 math math: quotientToInvariantsFunctor'_obj_V, res_quotientToInvariantsFunctor'_ι_hom_hom_apply, instPreservesZeroMorphismsQuotientToInvariantsFunctor', coind₁_quotientToInvariants_trivialCohomology, quotientToInvariantsFunctor'_obj_ρ, groupCohomology.quotientToInvariantsFunctor'_shortExact_ofShortExact, coind₁'_quotientToInvariants_trivialCohomology, quotientToInvariantsFunctor'_obj_ρ_apply, quotientToInvariantsFunctor'_obj_ρ_apply₂, groupCohomology.infl_δ_naturality
res_quotientToInvariantsFunctor'_ι 📖	CompOp	1 math math: res_quotientToInvariantsFunctor'_ι_hom_hom_apply
«term_↑_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesZeroMorphismsQuotientToInvariantsFunctor' 📖	mathematical	—	quotientToInvariantsFunctor'	—	—
quotientToInvariantsFunctor'_obj_V 📖	mathematical	—	quotientToInvariantsFunctor'	—	—
quotientToInvariantsFunctor'_obj_ρ 📖	mathematical	—	quotientToInvariantsFunctor'	—	—
quotientToInvariantsFunctor'_obj_ρ_apply 📖	mathematical	—	quotientToInvariantsFunctor'	—	QuotientGroup.quotientKerEquivOfSurjective_symm_apply
quotientToInvariantsFunctor'_obj_ρ_apply₂ 📖	mathematical	—	quotientToInvariantsFunctor'	—	quotientToInvariantsFunctor'_obj_ρ_apply
res_quotientToInvariantsFunctor'_ι_hom_hom_apply 📖	mathematical	—	res quotientToInvariantsFunctor' res_quotientToInvariantsFunctor'_ι	—	—

Rep.QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotientKerEquivOfSurjective_symm_apply 📖	—	—	—	—	—

groupCohomology

Definitions

Name	Category	Theorems
cochain_infl 📖	CompOp	—
infl 📖	CompOp	1 math math: infl_δ_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infl_δ_naturality 📖	mathematical	Rep.quotientToInvariantsFunctor' Rep.instPreservesZeroMorphismsQuotientToInvariantsFunctor'	Rep.quotientToInvariantsFunctor' Rep.instPreservesZeroMorphismsQuotientToInvariantsFunctor' infl	—	Rep.instPreservesZeroMorphismsQuotientToInvariantsFunctor'

---

← Back to Index