Map₁ comp ind₁' iso coind₁
Rep.map₁_comp_ind₁'_iso_coind₁'
Plain-language statement
Let M be a representation of a finite cyclic group G. Then the following square commutes coind₁'.obj M -------> coind₁'.obj M | | | | ↓ ↓ ind₁'.obj M -------> ind₁'.obj M The vertical maps are the canonical isomorphism ind₁'_iso_coind₁ and the horizontal maps are map₁ and map₂.
Exact Lean statement
lemma map₁_comp_ind₁'_iso_coind₁' :
map₁.app M ≫ (ind₁'_iso_coind₁'.app M).inv = (ind₁'_iso_coind₁'.app M).inv ≫ map₂.app MFormal artifact
Lean source
lemma map₁_comp_ind₁'_iso_coind₁' : map₁.app M ≫ (ind₁'_iso_coind₁'.app M).inv = (ind₁'_iso_coind₁'.app M).inv ≫ map₂.app M := by ext x simp only [coind₁', ind₁', Iso.app_inv, hom_comp, Representation.IntertwiningMap.comp_toLinearMap, LinearMap.coe_comp, Representation.IntertwiningMap.coe_toLinearMap, Function.comp_apply] at x ⊢ ext d simp only [ind₁'_iso_coind₁', Representation.ind₁'_lequiv_coind₁', linearEquivFunOnFinite, Equiv.invFun_as_coe, NatIso.ofComponents_inv_app, map₁, hom_ofHom, Representation.IntertwiningMap.coe_mk, Rep.mkIso_inv_hom_apply _, Representation.Equiv.mk_symm, Representation.Equiv.mk_apply, LinearEquiv.coe_symm_mk', equivFunOnFinite_symm_apply_apply, Representation.map₁_apply, map₂, Representation.map₂_apply_apply] congr classical simp [equivFunOnFinite, mapDomain, Finsupp.sum, Finsupp.single_apply, eq_comm (b := d), ← inv_mul_eq_iff_eq_mul]- Project
- Class Field Theory
- License
- Apache-2.0
- Commit
- f18cd7fd1575
- Source
- ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean:288-301
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Continuous algebra Map of density
continuous_algebraMap_of_density
Plain-language statement
Maddy's Lemma : Density implies continuity.
Source project: Class Field Theory
Person-level attribution pending.
Exists valuation algebra Map eq valuation pow
exists_valuation_algebraMap_eq_valuation_pow
Plain-language statement
Andrew's Lemma : Density for algebraic extensions.
Source project: Class Field Theory
Person-level attribution pending.
Exists of surjective
groupCohomology.exists_of_surjective
Plain-language statement
Given map f: M ⟶ N and q : ℕ, if H^{q+1}(M) ⟶ H^{q+1}(N) is surjective, then any z : Z^{q+1}(N) can be written as f(z') + d(y) for some z' : Z^{q+1}(M) and y : C^q(M). Note that d is spelled as toCocycles.
Source project: Class Field Theory
Person-level attribution pending.