Porting note: broken proof was · Issue #11039 · leanprover-community/mathlib4

mathlib4/Mathlib/RepresentationTheory/Rep.lean

Lines 225 to 236 in 5abbe68

    
           @[simp] 
        
           theorem linearization_μ_inv_hom (X Y : Action (Type u) (MonCat.of G)) : 
        
               (inv ((linearization k G).μ X Y)).hom = (finsuppTensorFinsupp' k X.V Y.V).symm.toLinearMap := by 
        
           -- Porting note (#11039): broken proof was 
        
           /-simp_rw [← Action.forget_map, Functor.map_inv, Action.forget_map, linearization_μ_hom] 
        
             apply IsIso.inv_eq_of_hom_inv_id _ 
        
             exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply _ _-/ 
        
             rw [← Action.forget_map, Functor.map_inv] 
        
             apply IsIso.inv_eq_of_hom_inv_id 
        
             exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply (finsuppTensorFinsupp' k X.V Y.V) x 
        
           set_option linter.uppercaseLean3 false in 
        
           #align Rep.linearization_μ_inv_hom Rep.linearization_μ_inv_hom

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Lines 123 to 170 in 5abbe68

    
           /- Porting note: linter says the statement doesn't typecheck, so we add `@[nolint checkType]` -/ 
        
           /-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is 
        
           morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains 
        
           and the homogeneous `linearYonedaObjResolution`. -/ 
        
           @[nolint checkType] theorem d_eq : 
        
               d n A = 
        
                 (diagonalHomEquiv n A).toModuleIso.inv ≫ 
        
                   (linearYonedaObjResolution A).d n (n + 1) ≫ 
        
                     (diagonalHomEquiv (n + 1) A).toModuleIso.hom := by 
        
             ext f g 
        
           /- Porting note (#11039): broken proof was 
        
             simp only [ModuleCat.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, 
        
               LinearEquiv.toModuleIso_inv, linearYonedaObjResolution_d_apply, LinearEquiv.toModuleIso_hom, 
        
               diagonalHomEquiv_apply, Action.comp_hom, Resolution.d_eq k G n, 
        
               Resolution.d_of (Fin.partialProd g), LinearMap.map_sum, 
        
               ← Finsupp.smul_single_one _ ((-1 : k) ^ _), map_smul, d_apply] 
        
             simp only [@Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero, 
        
               diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1)), Function.comp_apply, 
        
               Fin.partialProd_succ, Fin.castSucc_zero, Fin.partialProd_zero, one_mul] 
        
             congr 1 
        
             · congr 
        
               ext 
        
               have := Fin.partialProd_right_inv g (Fin.castSucc x) 
        
               simp only [mul_inv_rev, Fin.castSucc_fin_succ] at * 
        
               rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left] 
        
             · exact Finset.sum_congr rfl fun j hj => by 
        
                 rw [diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ] -/ 
        
             -- https://github.com/leanprover-community/mathlib4/issues/5026 
        
             -- https://github.com/leanprover-community/mathlib4/issues/5164 
        
             change d n A f g = diagonalHomEquiv (n + 1) A 
        
               ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g 
        
             -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
             erw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, 
        
               resolution.d_eq] 
        
             erw [resolution.d_of (Fin.partialProd g)] 
        
             simp only [map_sum, ← Finsupp.smul_single_one _ ((-1 : k) ^ _)] 
        
             -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
             erw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, 
        
               Fin.succAbove_zero, diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))] 
        
             simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero, 
        
               Fin.partialProd_zero, one_mul] 
        
             rcongr x 
        
             · have := Fin.partialProd_right_inv g (Fin.castSucc x) 
        
               simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢ 
        
               rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left] 
        
             · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
               erw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ] 
        
           #align inhomogeneous_cochains.d_eq inhomogeneousCochains.d_eq

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Lines 180 to 204 in 5abbe68

    
           /-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains 
        
           $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$ 
        
           which calculates the group cohomology of `A`. -/ 
        
           noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ := 
        
             CochainComplex.of (fun n => ModuleCat.of k ((Fin n → G) → A)) 
        
               (fun n => inhomogeneousCochains.d n A) fun n => by 
        
           /- Porting note (#11039): broken proof was 
        
               ext x y 
        
               have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2)) 
        
               simp only [ModuleCat.coe_comp, Function.comp_apply] at this 
        
               simp only [ModuleCat.coe_comp, Function.comp_apply, d_eq, LinearEquiv.toModuleIso_hom, 
        
                 LinearEquiv.toModuleIso_inv, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, this, 
        
                 LinearMap.zero_apply, map_zero, Pi.zero_apply] -/ 
        
               ext x 
        
               have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2)) 
        
               simp only [ModuleCat.comp_def, LinearMap.comp_apply] at this 
        
               dsimp only 
        
               simp only [d_eq, LinearEquiv.toModuleIso_inv, LinearEquiv.toModuleIso_hom, ModuleCat.coe_comp, 
        
                 Function.comp_apply] 
        
               /- Porting note: I can see I need to rewrite `LinearEquiv.coe_coe` twice to at 
        
                 least reduce the need for `symm_apply_apply` to be an `erw`. However, even `erw` refuses to 
        
                 rewrite the second `coe_coe`... -/ 
        
               erw [LinearEquiv.symm_apply_apply, this] 
        
               exact map_zero _ 
        
           #align group_cohomology.inhomogeneous_cochains groupCohomology.inhomogeneousCochains

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 108 to 127 in 5abbe68

    
           theorem actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) : 
        
               (actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) := by 
        
             induction' n with n hn 
        
             · exact Prod.ext rfl (funext fun x => Fin.elim0 x) 
        
             · refine' Prod.ext rfl (funext fun x => _) 
        
           /- Porting note (#11039): broken proof was 
        
               · dsimp only [actionDiagonalSucc] 
        
                 simp only [Iso.trans_hom, comp_hom, types_comp_apply, diagonalSucc_hom_hom, 
        
                   leftRegularTensorIso_hom_hom, tensorIso_hom, mkIso_hom_hom, Equiv.toIso_hom, 
        
                   Action.tensorHom, Equiv.piFinSuccAbove_symm_apply, tensor_apply, types_id_apply, 
        
                   tensor_rho, MonoidHom.one_apply, End.one_def, hn fun j : Fin (n + 1) => f j.succ, 
        
                   Fin.insertNth_zero'] 
        
                 refine' Fin.cases (Fin.cons_zero _ _) (fun i => _) x 
        
                 · simp only [Fin.cons_succ, mul_left_inj, inv_inj, Fin.castSucc_fin_succ] -/ 
        
               · dsimp [actionDiagonalSucc] 
        
                 erw [hn (fun (j : Fin (n + 1)) => f j.succ)] 
        
                 exact Fin.cases rfl (fun i => rfl) x 
        
           set_option linter.uppercaseLean3 false in 
        
           #align group_cohomology.resolution.Action_diagonal_succ_hom_apply groupCohomology.resolution.actionDiagonalSucc_hom_apply

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 128 to 156 in 5abbe68

    
           theorem actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) : 
        
               (actionDiagonalSucc G n).inv.hom (g, f) = (g • Fin.partialProd f : Fin (n + 1) → G) := by 
        
             revert g 
        
             induction' n with n hn 
        
             · intro g 
        
               funext (x : Fin 1) 
        
               simp only [Subsingleton.elim x 0, Pi.smul_apply, Fin.partialProd_zero, smul_eq_mul, mul_one] 
        
               rfl 
        
             · intro g 
        
           /- Porting note (#11039): broken proof was 
        
               ext 
        
               dsimp only [actionDiagonalSucc] 
        
               simp only [Iso.trans_inv, comp_hom, hn, diagonalSucc_inv_hom, types_comp_apply, tensorIso_inv, 
        
                 Iso.refl_inv, Action.tensorHom, id_hom, tensor_apply, types_id_apply, 
        
                 leftRegularTensorIso_inv_hom, tensor_rho, leftRegular_ρ_apply, Pi.smul_apply, smul_eq_mul] 
        
               refine' Fin.cases _ _ x 
        
               · simp only [Fin.cons_zero, Fin.partialProd_zero, mul_one] 
        
               · intro i 
        
                 simpa only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', mul_assoc] -/ 
        
               funext x 
        
               dsimp [actionDiagonalSucc] 
        
               erw [hn, Equiv.piFinSuccAbove_symm_apply] 
        
               refine' Fin.cases _ (fun i => _) x 
        
               · simp only [Fin.insertNth_zero, Fin.cons_zero, Fin.partialProd_zero, mul_one] 
        
               · simp only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', ← mul_assoc] 
        
                 rfl 
        
           set_option linter.uppercaseLean3 false in 
        
           #align group_cohomology.resolution.Action_diagonal_succ_inv_apply groupCohomology.resolution.actionDiagonalSucc_inv_apply

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 176 to 199 in 5abbe68

    
           theorem diagonalSucc_hom_single (f : Gⁿ⁺¹) (a : k) : 
        
               (diagonalSucc k G n).hom.hom (single f a) = 
        
                 single (f 0) 1 ⊗ₜ single (fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) a := by 
        
           /- Porting note (#11039): broken proof was 
        
             dsimp only [diagonalSucc] 
        
             simpa only [Iso.trans_hom, Iso.symm_hom, Action.comp_hom, ModuleCat.comp_def, 
        
               LinearMap.comp_apply, Functor.mapIso_hom, 
        
               linearization_map_hom_single (actionDiagonalSucc G n).hom f a, asIso_inv, 
        
               linearization_μ_inv_hom, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp', 
        
               LinearEquiv.trans_symm, lcongr_symm, LinearEquiv.trans_apply, lcongr_single, 
        
               TensorProduct.lid_symm_apply, finsuppTensorFinsupp_symm_single, LinearEquiv.coe_toLinearMap] -/ 
        
             change (𝟙 ((linearization k G).1.obj (Action.leftRegular G)).V 
        
                 ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) 
        
               ((inv ((linearization k G).μ (Action.leftRegular G) { V := Fin n → G, ρ := 1 })).hom 
        
                 ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) = _ 
        
             simp only [CategoryTheory.Functor.map_id, linearization_μ_inv_hom] 
        
             -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
             erw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp', 
        
               LinearEquiv.trans_symm, LinearEquiv.trans_apply, lcongr_symm, Equiv.refl_symm] 
        
             erw [lcongr_single] 
        
             rw [TensorProduct.lid_symm_apply, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp_symm_single] 
        
             rfl 
        
           #align group_cohomology.resolution.diagonal_succ_hom_single groupCohomology.resolution.diagonalSucc_hom_single

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 200 to 220 in 5abbe68

    
           theorem diagonalSucc_inv_single_single (g : G) (f : Gⁿ) (a b : k) : 
        
               (diagonalSucc k G n).inv.hom (Finsupp.single g a ⊗ₜ Finsupp.single f b) = 
        
                 single (g • partialProd f) (a * b) := by 
        
           /- Porting note (#11039): broken proof was 
        
             dsimp only [diagonalSucc] 
        
             simp only [Iso.trans_inv, Iso.symm_inv, Iso.refl_inv, tensorIso_inv, Action.tensorHom, 
        
               Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, asIso_hom, Functor.mapIso_inv, 
        
               ModuleCat.MonoidalCategory.hom_apply, linearizationTrivialIso_inv_hom_apply, 
        
               linearization_μ_hom, Action.id_hom ((linearization k G).obj _), actionDiagonalSucc_inv_apply, 
        
               ModuleCat.id_apply, LinearEquiv.coe_toLinearMap, 
        
               finsuppTensorFinsupp'_single_tmul_single k (Action.leftRegular G).V, 
        
               linearization_map_hom_single (actionDiagonalSucc G n).inv (g, f) (a * b)] -/ 
        
             change mapDomain (actionDiagonalSucc G n).inv.hom 
        
               (lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k) 
        
                 (finsuppTensorFinsupp k k k G (Fin n → G) (single g a ⊗ₜ[k] single f b))) 
        
               = single (g • partialProd f) (a * b) 
        
             rw [finsuppTensorFinsupp_single, lcongr_single, mapDomain_single, Equiv.refl_apply, 
        
               actionDiagonalSucc_inv_apply] 
        
             rfl 
        
           #align group_cohomology.resolution.diagonal_succ_inv_single_single groupCohomology.resolution.diagonalSucc_inv_single_single

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 221 to 242 in 5abbe68

    
           theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) : 
        
               (diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ f) = 
        
                 Finsupp.lift (Gⁿ⁺¹ →₀ k) k Gⁿ (fun f => single (g • partialProd f) r) f := by 
        
             refine f.induction ?_ ?_ 
        
           /- Porting note (#11039): broken proof was 
        
             · simp only [TensorProduct.tmul_zero, map_zero] 
        
             · intro a b x ha hb hx 
        
               simp only [lift_apply, smul_single', mul_one, TensorProduct.tmul_add, map_add, 
        
                 diagonalSucc_inv_single_single, hx, Finsupp.sum_single_index, mul_comm b, 
        
                 zero_mul, single_zero] -/ 
        
             · rw [TensorProduct.tmul_zero, map_zero] 
        
               -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
               erw [map_zero] 
        
             · intro _ _ _ _ _ hx 
        
               rw [TensorProduct.tmul_add, map_add]; erw [map_add, hx] 
        
               simp_rw [lift_apply, smul_single, smul_eq_mul] 
        
               -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
               erw [diagonalSucc_inv_single_single] 
        
               rw [sum_single_index, mul_comm] 
        
               · rw [zero_mul, single_zero] 
        
           #align group_cohomology.resolution.diagonal_succ_inv_single_left groupCohomology.resolution.diagonalSucc_inv_single_left

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 243 to 263 in 5abbe68

    
           theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) : 
        
               (diagonalSucc k G n).inv.hom (g ⊗ₜ Finsupp.single f r) = 
        
                 Finsupp.lift _ k G (fun a => single (a • partialProd f) r) g := by 
        
             refine g.induction ?_ ?_ 
        
           /- Porting note (#11039): broken proof was 
        
             · simp only [TensorProduct.zero_tmul, map_zero] 
        
             · intro a b x ha hb hx 
        
               simp only [lift_apply, smul_single', map_add, hx, diagonalSucc_inv_single_single, 
        
                 TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero] -/ 
        
             · rw [TensorProduct.zero_tmul, map_zero] 
        
               -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
               erw [map_zero] 
        
             · intro _ _ _ _ _ hx 
        
               rw [TensorProduct.add_tmul, map_add]; erw [map_add, hx] 
        
               simp_rw [lift_apply, smul_single'] 
        
               -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
               erw [diagonalSucc_inv_single_single] 
        
               rw [sum_single_index] 
        
               · rw [zero_mul, single_zero] 
        
           #align group_cohomology.resolution.diagonal_succ_inv_single_right groupCohomology.resolution.diagonalSucc_inv_single_right

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 270 to 297 in 5abbe68

    
           /-- The `k[G]`-linear isomorphism `k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹]`, where the `k[G]`-module structure on 
        
           the lefthand side is `TensorProduct.leftModule`, whilst that of the righthand side comes from 
        
           `Representation.asModule`. Allows us to use `Algebra.TensorProduct.basis` to get a `k[G]`-basis 
        
           of the righthand side. -/ 
        
           def ofMulActionBasisAux : 
        
               MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k) ≃ₗ[MonoidAlgebra k G] 
        
                 (ofMulAction k G (Fin (n + 1) → G)).asModule := 
        
             { (Rep.equivalenceModuleMonoidAlgebra.1.mapIso (diagonalSucc k G n).symm).toLinearEquiv with 
        
               map_smul' := fun r x => by 
        
                 -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
                 erw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul] 
        
                 congr 1 
        
           /- Porting note (#11039): broken proof was 
        
                 refine' x.induction_on _ (fun x y => _) fun y z hy hz => _ 
        
                 · simp only [smul_zero] 
        
                 · simp only [TensorProduct.smul_tmul'] 
        
                   show (r * x) ⊗ₜ y = _ 
        
                   rw [← ofMulAction_self_smul_eq_mul, smul_tprod_one_asModule] 
        
                 · rw [smul_add, hz, hy, smul_add] -/ 
        
                 show _ = Representation.asAlgebraHom (tensorObj (Rep.leftRegular k G) 
        
                   (Rep.trivial k G ((Fin n → G) →₀ k))).ρ r _ 
        
                 refine' x.induction_on _ (fun x y => _) fun y z hy hz => _ 
        
                 · rw [smul_zero, map_zero] 
        
                 · rw [TensorProduct.smul_tmul', smul_eq_mul, ← ofMulAction_self_smul_eq_mul] 
        
                   exact (smul_tprod_one_asModule (Representation.ofMulAction k G G) r x y).symm 
        
                 · rw [smul_add, hz, hy, map_add] } 
        
           #align group_cohomology.resolution.of_mul_action_basis_aux groupCohomology.resolution.ofMulActionBasisAux

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 337 to 353 in 5abbe68

    
           /-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of 
        
           the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that this 
        
           sends a morphism of representations `f : k[Gⁿ⁺¹] ⟶ A` to the function 
        
           `(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).` -/ 
        
           theorem diagonalHomEquiv_apply (f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) (x : Fin n → G) : 
        
               diagonalHomEquiv n A f x = f.hom (Finsupp.single (Fin.partialProd x) 1) := by 
        
           /- Porting note (#11039): broken proof was 
        
             unfold diagonalHomEquiv 
        
             simpa only [LinearEquiv.trans_apply, Rep.leftRegularHomEquiv_apply, 
        
               MonoidalClosed.linearHomEquivComm_hom, Finsupp.llift_symm_apply, TensorProduct.curry_apply, 
        
               Linear.homCongr_apply, Iso.refl_hom, Iso.trans_inv, Action.comp_hom, ModuleCat.comp_def, 
        
               LinearMap.comp_apply, Representation.repOfTprodIso_inv_apply, 
        
               diagonalSucc_inv_single_single (1 : G) x, one_smul, one_mul] -/ 
        
             change f.hom ((diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) = _ 
        
             rw [diagonalSucc_inv_single_single, one_smul, one_mul] 
        
           set_option linter.uppercaseLean3 false in 
        
           #align Rep.diagonal_hom_equiv_apply Rep.diagonalHomEquiv_apply

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 355 to 393 in 5abbe68

    
           /-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of 
        
           the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that the 
        
           inverse map sends a function `f : Gⁿ → A` to the representation morphism sending 
        
           `(g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`, where `ρ` is the representation attached 
        
           to `A`. -/ 
        
           theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1) → G) : 
        
               ((diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) = 
        
                 A.ρ (x 0) (f fun i : Fin n => (x (Fin.castSucc i))⁻¹ * x i.succ) := by 
        
             unfold diagonalHomEquiv 
        
           /- Porting note (#11039): broken proof was 
        
             simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply, 
        
               Rep.leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Action.comp_hom, Iso.refl_inv, 
        
               Category.comp_id, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Iso.trans_hom, 
        
               ModuleCat.comp_def, LinearMap.comp_apply, Representation.repOfTprodIso_apply, 
        
               diagonalSucc_hom_single x (1 : k), TensorProduct.uncurry_apply, Rep.leftRegularHom_hom, 
        
               Finsupp.lift_apply, ihom_obj_ρ_def, Rep.ihom_obj_ρ_apply, Finsupp.sum_single_index, zero_smul, 
        
               one_smul, Rep.of_ρ, Rep.Action_ρ_eq_ρ, Rep.trivial_def (x 0)⁻¹, Finsupp.llift_apply A k k] -/ 
        
             simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply, 
        
               leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Iso.trans_hom, Iso.refl_inv, 
        
               Category.comp_id, Action.comp_hom, MonoidalClosed.linearHomEquivComm_symm_hom] 
        
             -- Porting note: This is a sure sign that coercions for morphisms in `ModuleCat` 
        
             -- are still not set up properly. 
        
             -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
             erw [ModuleCat.coe_comp] 
        
             simp only [ModuleCat.coe_comp, Function.comp_apply] 
        
             -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 
        
             erw [diagonalSucc_hom_single] 
        
             erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index] 
        
             simp only [one_smul] 
        
             erw [Representation.linHom_apply] 
        
             simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply] 
        
             erw [Finsupp.llift_apply] 
        
             rw [Finsupp.lift_apply] 
        
             erw [Finsupp.sum_single_index] 
        
             rw [one_smul] 
        
             · rw [zero_smul] 
        
             · rw [zero_smul] 
        
           set_option linter.uppercaseLean3 false in 
        
           #align Rep.diagonal_hom_equiv_symm_apply Rep.diagonalHomEquiv_symm_apply

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Lines 553 to 571 in 5abbe68

    
           /-- Simpler expression for the differential in the standard resolution of `k` as a 
        
           `G`-representation. It sends `(g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁)`. -/ 
        
           theorem d_eq (n : ℕ) : ((groupCohomology.resolution k G).d (n + 1) n).hom = d k G (n + 1) := by 
        
             refine' Finsupp.lhom_ext' fun x => LinearMap.ext_ring _ 
        
             dsimp [groupCohomology.resolution] 
        
           /- Porting note (#11039): broken proof was 
        
             simpa [← @intCast_smul k, simplicial_object.δ] -/ 
        
             simp_rw [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, SimplicialObject.δ, 
        
               Functor.comp_map, ← intCast_smul (k := k) ((-1) ^ _ : ℤ), Int.cast_pow, Int.cast_neg, 
        
               Int.cast_one, Action.sum_hom, Action.smul_hom, Rep.linearization_map_hom] 
        
             rw [LinearMap.coeFn_sum, Fintype.sum_apply] 
        
             erw [d_of (k := k) x] 
        
           /- Porting note: want to rewrite `LinearMap.smul_apply` but simp/simp_rw won't do it; I need erw, 
        
           so using Finset.sum_congr to get rid of the binder -/ 
        
             refine' Finset.sum_congr rfl fun _ _ => _ 
        
             erw [LinearMap.smul_apply] 
        
             rw [Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, Finsupp.smul_single', mul_one] 
        
             rfl 
        
           #align group_cohomology.resolution.d_eq groupCohomology.resolution.d_eq

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Porting note: broken proof was #11039

Examples

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	@[simp]
	theorem linearization_μ_inv_hom (X Y : Action (Type u) (MonCat.of G)) :
	(inv ((linearization k G).μ X Y)).hom = (finsuppTensorFinsupp' k X.V Y.V).symm.toLinearMap := by
	-- Porting note (#11039): broken proof was
	/-simp_rw [← Action.forget_map, Functor.map_inv, Action.forget_map, linearization_μ_hom]
	apply IsIso.inv_eq_of_hom_inv_id _
	exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply _ _-/
	rw [← Action.forget_map, Functor.map_inv]
	apply IsIso.inv_eq_of_hom_inv_id
	exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply (finsuppTensorFinsupp' k X.V Y.V) x
	set_option linter.uppercaseLean3 false in
	#align Rep.linearization_μ_inv_hom Rep.linearization_μ_inv_hom

	/- Porting note: linter says the statement doesn't typecheck, so we add `@[nolint checkType]` -/
	/-- The theorem that our isomorphism `Fun(Gⁿ, A) ≅ Hom(k[Gⁿ⁺¹], A)` (where the righthand side is
	morphisms in `Rep k G`) commutes with the differentials in the complex of inhomogeneous cochains
	and the homogeneous `linearYonedaObjResolution`. -/
	@[nolint checkType] theorem d_eq :
	d n A =
	(diagonalHomEquiv n A).toModuleIso.inv ≫
	(linearYonedaObjResolution A).d n (n + 1) ≫
	(diagonalHomEquiv (n + 1) A).toModuleIso.hom := by
	ext f g
	/- Porting note (#11039): broken proof was
	simp only [ModuleCat.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
	LinearEquiv.toModuleIso_inv, linearYonedaObjResolution_d_apply, LinearEquiv.toModuleIso_hom,
	diagonalHomEquiv_apply, Action.comp_hom, Resolution.d_eq k G n,
	Resolution.d_of (Fin.partialProd g), LinearMap.map_sum,
	← Finsupp.smul_single_one _ ((-1 : k) ^ _), map_smul, d_apply]
	simp only [@Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul, Fin.succAbove_zero,
	diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1)), Function.comp_apply,
	Fin.partialProd_succ, Fin.castSucc_zero, Fin.partialProd_zero, one_mul]
	congr 1
	· congr
	ext
	have := Fin.partialProd_right_inv g (Fin.castSucc x)
	simp only [mul_inv_rev, Fin.castSucc_fin_succ] at *
	rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left]
	· exact Finset.sum_congr rfl fun j hj => by
	rw [diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ] -/
	-- https://github.com/leanprover-community/mathlib4/issues/5026
	-- https://github.com/leanprover-community/mathlib4/issues/5164
	change d n A f g = diagonalHomEquiv (n + 1) A
	((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [diagonalHomEquiv_apply, Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply,
	resolution.d_eq]
	erw [resolution.d_of (Fin.partialProd g)]
	simp only [map_sum, ← Finsupp.smul_single_one _ ((-1 : k) ^ _)]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [d_apply, @Fin.sum_univ_succ _ _ (n + 1), Fin.val_zero, pow_zero, one_smul,
	Fin.succAbove_zero, diagonalHomEquiv_symm_apply f (Fin.partialProd g ∘ @Fin.succ (n + 1))]
	simp_rw [Function.comp_apply, Fin.partialProd_succ, Fin.castSucc_zero,
	Fin.partialProd_zero, one_mul]
	rcongr x
	· have := Fin.partialProd_right_inv g (Fin.castSucc x)
	simp only [mul_inv_rev, Fin.castSucc_fin_succ] at this ⊢
	rw [mul_assoc, ← mul_assoc _ _ (g x.succ), this, inv_mul_cancel_left]
	· -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ]
	#align inhomogeneous_cochains.d_eq inhomogeneousCochains.d_eq

	/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains
	$$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
	which calculates the group cohomology of `A`. -/
	noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ :=
	CochainComplex.of (fun n => ModuleCat.of k ((Fin n → G) → A))
	(fun n => inhomogeneousCochains.d n A) fun n => by
	/- Porting note (#11039): broken proof was
	ext x y
	have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2))
	simp only [ModuleCat.coe_comp, Function.comp_apply] at this
	simp only [ModuleCat.coe_comp, Function.comp_apply, d_eq, LinearEquiv.toModuleIso_hom,
	LinearEquiv.toModuleIso_inv, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, this,
	LinearMap.zero_apply, map_zero, Pi.zero_apply] -/
	ext x
	have := LinearMap.ext_iff.1 ((linearYonedaObjResolution A).d_comp_d n (n + 1) (n + 2))
	simp only [ModuleCat.comp_def, LinearMap.comp_apply] at this
	dsimp only
	simp only [d_eq, LinearEquiv.toModuleIso_inv, LinearEquiv.toModuleIso_hom, ModuleCat.coe_comp,
	Function.comp_apply]
	/- Porting note: I can see I need to rewrite `LinearEquiv.coe_coe` twice to at
	least reduce the need for `symm_apply_apply` to be an `erw`. However, even `erw` refuses to
	rewrite the second `coe_coe`... -/
	erw [LinearEquiv.symm_apply_apply, this]
	exact map_zero _
	#align group_cohomology.inhomogeneous_cochains groupCohomology.inhomogeneousCochains

	theorem actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (n + 1) → G) :
	(actionDiagonalSucc G n).hom.hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) := by
	induction' n with n hn
	· exact Prod.ext rfl (funext fun x => Fin.elim0 x)
	· refine' Prod.ext rfl (funext fun x => _)
	/- Porting note (#11039): broken proof was
	· dsimp only [actionDiagonalSucc]
	simp only [Iso.trans_hom, comp_hom, types_comp_apply, diagonalSucc_hom_hom,
	leftRegularTensorIso_hom_hom, tensorIso_hom, mkIso_hom_hom, Equiv.toIso_hom,
	Action.tensorHom, Equiv.piFinSuccAbove_symm_apply, tensor_apply, types_id_apply,
	tensor_rho, MonoidHom.one_apply, End.one_def, hn fun j : Fin (n + 1) => f j.succ,
	Fin.insertNth_zero']
	refine' Fin.cases (Fin.cons_zero _ _) (fun i => _) x
	· simp only [Fin.cons_succ, mul_left_inj, inv_inj, Fin.castSucc_fin_succ] -/
	· dsimp [actionDiagonalSucc]
	erw [hn (fun (j : Fin (n + 1)) => f j.succ)]
	exact Fin.cases rfl (fun i => rfl) x
	set_option linter.uppercaseLean3 false in
	#align group_cohomology.resolution.Action_diagonal_succ_hom_apply groupCohomology.resolution.actionDiagonalSucc_hom_apply

	theorem actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f : Fin n → G) :
	(actionDiagonalSucc G n).inv.hom (g, f) = (g • Fin.partialProd f : Fin (n + 1) → G) := by
	revert g
	induction' n with n hn
	· intro g
	funext (x : Fin 1)
	simp only [Subsingleton.elim x 0, Pi.smul_apply, Fin.partialProd_zero, smul_eq_mul, mul_one]
	rfl
	· intro g
	/- Porting note (#11039): broken proof was
	ext
	dsimp only [actionDiagonalSucc]
	simp only [Iso.trans_inv, comp_hom, hn, diagonalSucc_inv_hom, types_comp_apply, tensorIso_inv,
	Iso.refl_inv, Action.tensorHom, id_hom, tensor_apply, types_id_apply,
	leftRegularTensorIso_inv_hom, tensor_rho, leftRegular_ρ_apply, Pi.smul_apply, smul_eq_mul]
	refine' Fin.cases _ _ x
	· simp only [Fin.cons_zero, Fin.partialProd_zero, mul_one]
	· intro i
	simpa only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', mul_assoc] -/
	funext x
	dsimp [actionDiagonalSucc]
	erw [hn, Equiv.piFinSuccAbove_symm_apply]
	refine' Fin.cases _ (fun i => _) x
	· simp only [Fin.insertNth_zero, Fin.cons_zero, Fin.partialProd_zero, mul_one]
	· simp only [Fin.cons_succ, Pi.smul_apply, smul_eq_mul, Fin.partialProd_succ', ← mul_assoc]
	rfl
	set_option linter.uppercaseLean3 false in
	#align group_cohomology.resolution.Action_diagonal_succ_inv_apply groupCohomology.resolution.actionDiagonalSucc_inv_apply

	theorem diagonalSucc_hom_single (f : Gⁿ⁺¹) (a : k) :
	(diagonalSucc k G n).hom.hom (single f a) =
	single (f 0) 1 ⊗ₜ single (fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) a := by
	/- Porting note (#11039): broken proof was
	dsimp only [diagonalSucc]
	simpa only [Iso.trans_hom, Iso.symm_hom, Action.comp_hom, ModuleCat.comp_def,
	LinearMap.comp_apply, Functor.mapIso_hom,
	linearization_map_hom_single (actionDiagonalSucc G n).hom f a, asIso_inv,
	linearization_μ_inv_hom, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp',
	LinearEquiv.trans_symm, lcongr_symm, LinearEquiv.trans_apply, lcongr_single,
	TensorProduct.lid_symm_apply, finsuppTensorFinsupp_symm_single, LinearEquiv.coe_toLinearMap] -/
	change (𝟙 ((linearization k G).1.obj (Action.leftRegular G)).V
	⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom)
	((inv ((linearization k G).μ (Action.leftRegular G) { V := Fin n → G, ρ := 1 })).hom
	((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) = _
	simp only [CategoryTheory.Functor.map_id, linearization_μ_inv_hom]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [lmapDomain_apply, mapDomain_single, LinearEquiv.coe_toLinearMap, finsuppTensorFinsupp',
	LinearEquiv.trans_symm, LinearEquiv.trans_apply, lcongr_symm, Equiv.refl_symm]
	erw [lcongr_single]
	rw [TensorProduct.lid_symm_apply, actionDiagonalSucc_hom_apply, finsuppTensorFinsupp_symm_single]
	rfl
	#align group_cohomology.resolution.diagonal_succ_hom_single groupCohomology.resolution.diagonalSucc_hom_single

	theorem diagonalSucc_inv_single_single (g : G) (f : Gⁿ) (a b : k) :
	(diagonalSucc k G n).inv.hom (Finsupp.single g a ⊗ₜ Finsupp.single f b) =
	single (g • partialProd f) (a * b) := by
	/- Porting note (#11039): broken proof was
	dsimp only [diagonalSucc]
	simp only [Iso.trans_inv, Iso.symm_inv, Iso.refl_inv, tensorIso_inv, Action.tensorHom,
	Action.comp_hom, ModuleCat.comp_def, LinearMap.comp_apply, asIso_hom, Functor.mapIso_inv,
	ModuleCat.MonoidalCategory.hom_apply, linearizationTrivialIso_inv_hom_apply,
	linearization_μ_hom, Action.id_hom ((linearization k G).obj _), actionDiagonalSucc_inv_apply,
	ModuleCat.id_apply, LinearEquiv.coe_toLinearMap,
	finsuppTensorFinsupp'_single_tmul_single k (Action.leftRegular G).V,
	linearization_map_hom_single (actionDiagonalSucc G n).inv (g, f) (a * b)] -/
	change mapDomain (actionDiagonalSucc G n).inv.hom
	(lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k)
	(finsuppTensorFinsupp k k k G (Fin n → G) (single g a ⊗ₜ[k] single f b)))
	= single (g • partialProd f) (a * b)
	rw [finsuppTensorFinsupp_single, lcongr_single, mapDomain_single, Equiv.refl_apply,
	actionDiagonalSucc_inv_apply]
	rfl
	#align group_cohomology.resolution.diagonal_succ_inv_single_single groupCohomology.resolution.diagonalSucc_inv_single_single

	theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) :
	(diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ f) =
	Finsupp.lift (Gⁿ⁺¹ →₀ k) k Gⁿ (fun f => single (g • partialProd f) r) f := by
	refine f.induction ?_ ?_
	/- Porting note (#11039): broken proof was
	· simp only [TensorProduct.tmul_zero, map_zero]
	· intro a b x ha hb hx
	simp only [lift_apply, smul_single', mul_one, TensorProduct.tmul_add, map_add,
	diagonalSucc_inv_single_single, hx, Finsupp.sum_single_index, mul_comm b,
	zero_mul, single_zero] -/
	· rw [TensorProduct.tmul_zero, map_zero]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [map_zero]
	· intro _ _ _ _ _ hx
	rw [TensorProduct.tmul_add, map_add]; erw [map_add, hx]
	simp_rw [lift_apply, smul_single, smul_eq_mul]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [diagonalSucc_inv_single_single]
	rw [sum_single_index, mul_comm]
	· rw [zero_mul, single_zero]
	#align group_cohomology.resolution.diagonal_succ_inv_single_left groupCohomology.resolution.diagonalSucc_inv_single_left

	theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) :
	(diagonalSucc k G n).inv.hom (g ⊗ₜ Finsupp.single f r) =
	Finsupp.lift _ k G (fun a => single (a • partialProd f) r) g := by
	refine g.induction ?_ ?_
	/- Porting note (#11039): broken proof was
	· simp only [TensorProduct.zero_tmul, map_zero]
	· intro a b x ha hb hx
	simp only [lift_apply, smul_single', map_add, hx, diagonalSucc_inv_single_single,
	TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero] -/
	· rw [TensorProduct.zero_tmul, map_zero]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [map_zero]
	· intro _ _ _ _ _ hx
	rw [TensorProduct.add_tmul, map_add]; erw [map_add, hx]
	simp_rw [lift_apply, smul_single']
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [diagonalSucc_inv_single_single]
	rw [sum_single_index]
	· rw [zero_mul, single_zero]
	#align group_cohomology.resolution.diagonal_succ_inv_single_right groupCohomology.resolution.diagonalSucc_inv_single_right

	/-- The `k[G]`-linear isomorphism `k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹]`, where the `k[G]`-module structure on
	the lefthand side is `TensorProduct.leftModule`, whilst that of the righthand side comes from
	`Representation.asModule`. Allows us to use `Algebra.TensorProduct.basis` to get a `k[G]`-basis
	of the righthand side. -/
	def ofMulActionBasisAux :
	MonoidAlgebra k G ⊗[k] ((Fin n → G) →₀ k) ≃ₗ[MonoidAlgebra k G]
	(ofMulAction k G (Fin (n + 1) → G)).asModule :=
	{ (Rep.equivalenceModuleMonoidAlgebra.1.mapIso (diagonalSucc k G n).symm).toLinearEquiv with
	map_smul' := fun r x => by
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [RingHom.id_apply, LinearEquiv.toFun_eq_coe, ← LinearEquiv.map_smul]
	congr 1
	/- Porting note (#11039): broken proof was
	refine' x.induction_on _ (fun x y => _) fun y z hy hz => _
	· simp only [smul_zero]
	· simp only [TensorProduct.smul_tmul']
	show (r * x) ⊗ₜ y = _
	rw [← ofMulAction_self_smul_eq_mul, smul_tprod_one_asModule]
	· rw [smul_add, hz, hy, smul_add] -/
	show _ = Representation.asAlgebraHom (tensorObj (Rep.leftRegular k G)
	(Rep.trivial k G ((Fin n → G) →₀ k))).ρ r _
	refine' x.induction_on _ (fun x y => _) fun y z hy hz => _
	· rw [smul_zero, map_zero]
	· rw [TensorProduct.smul_tmul', smul_eq_mul, ← ofMulAction_self_smul_eq_mul]
	exact (smul_tprod_one_asModule (Representation.ofMulAction k G G) r x y).symm
	· rw [smul_add, hz, hy, map_add] }
	#align group_cohomology.resolution.of_mul_action_basis_aux groupCohomology.resolution.ofMulActionBasisAux

	/-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of
	the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that this
	sends a morphism of representations `f : k[Gⁿ⁺¹] ⟶ A` to the function
	`(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).` -/
	theorem diagonalHomEquiv_apply (f : Rep.ofMulAction k G (Fin (n + 1) → G) ⟶ A) (x : Fin n → G) :
	diagonalHomEquiv n A f x = f.hom (Finsupp.single (Fin.partialProd x) 1) := by
	/- Porting note (#11039): broken proof was
	unfold diagonalHomEquiv
	simpa only [LinearEquiv.trans_apply, Rep.leftRegularHomEquiv_apply,
	MonoidalClosed.linearHomEquivComm_hom, Finsupp.llift_symm_apply, TensorProduct.curry_apply,
	Linear.homCongr_apply, Iso.refl_hom, Iso.trans_inv, Action.comp_hom, ModuleCat.comp_def,
	LinearMap.comp_apply, Representation.repOfTprodIso_inv_apply,
	diagonalSucc_inv_single_single (1 : G) x, one_smul, one_mul] -/
	change f.hom ((diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) = _
	rw [diagonalSucc_inv_single_single, one_smul, one_mul]
	set_option linter.uppercaseLean3 false in
	#align Rep.diagonal_hom_equiv_apply Rep.diagonalHomEquiv_apply

	/-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of
	the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that the
	inverse map sends a function `f : Gⁿ → A` to the representation morphism sending
	`(g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`, where `ρ` is the representation attached
	to `A`. -/
	theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1) → G) :
	((diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) =
	A.ρ (x 0) (f fun i : Fin n => (x (Fin.castSucc i))⁻¹ * x i.succ) := by
	unfold diagonalHomEquiv
	/- Porting note (#11039): broken proof was
	simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
	Rep.leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Action.comp_hom, Iso.refl_inv,
	Category.comp_id, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Iso.trans_hom,
	ModuleCat.comp_def, LinearMap.comp_apply, Representation.repOfTprodIso_apply,
	diagonalSucc_hom_single x (1 : k), TensorProduct.uncurry_apply, Rep.leftRegularHom_hom,
	Finsupp.lift_apply, ihom_obj_ρ_def, Rep.ihom_obj_ρ_apply, Finsupp.sum_single_index, zero_smul,
	one_smul, Rep.of_ρ, Rep.Action_ρ_eq_ρ, Rep.trivial_def (x 0)⁻¹, Finsupp.llift_apply A k k] -/
	simp only [LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
	leftRegularHomEquiv_symm_apply, Linear.homCongr_symm_apply, Iso.trans_hom, Iso.refl_inv,
	Category.comp_id, Action.comp_hom, MonoidalClosed.linearHomEquivComm_symm_hom]
	-- Porting note: This is a sure sign that coercions for morphisms in `ModuleCat`
	-- are still not set up properly.
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [ModuleCat.coe_comp]
	simp only [ModuleCat.coe_comp, Function.comp_apply]
	-- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
	erw [diagonalSucc_hom_single]
	erw [TensorProduct.uncurry_apply, Finsupp.lift_apply, Finsupp.sum_single_index]
	simp only [one_smul]
	erw [Representation.linHom_apply]
	simp only [LinearMap.comp_apply, MonoidHom.one_apply, LinearMap.one_apply]
	erw [Finsupp.llift_apply]
	rw [Finsupp.lift_apply]
	erw [Finsupp.sum_single_index]
	rw [one_smul]
	· rw [zero_smul]
	· rw [zero_smul]
	set_option linter.uppercaseLean3 false in
	#align Rep.diagonal_hom_equiv_symm_apply Rep.diagonalHomEquiv_symm_apply

	/-- Simpler expression for the differential in the standard resolution of `k` as a
	`G`-representation. It sends `(g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁)`. -/
	theorem d_eq (n : ℕ) : ((groupCohomology.resolution k G).d (n + 1) n).hom = d k G (n + 1) := by
	refine' Finsupp.lhom_ext' fun x => LinearMap.ext_ring _
	dsimp [groupCohomology.resolution]
	/- Porting note (#11039): broken proof was
	simpa [← @intCast_smul k, simplicial_object.δ] -/
	simp_rw [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, SimplicialObject.δ,
	Functor.comp_map, ← intCast_smul (k := k) ((-1) ^ _ : ℤ), Int.cast_pow, Int.cast_neg,
	Int.cast_one, Action.sum_hom, Action.smul_hom, Rep.linearization_map_hom]
	rw [LinearMap.coeFn_sum, Fintype.sum_apply]
	erw [d_of (k := k) x]
	/- Porting note: want to rewrite `LinearMap.smul_apply` but simp/simp_rw won't do it; I need erw,
	so using Finset.sum_congr to get rid of the binder -/
	refine' Finset.sum_congr rfl fun _ _ => _
	erw [LinearMap.smul_apply]
	rw [Finsupp.lmapDomain_apply, Finsupp.mapDomain_single, Finsupp.smul_single', mul_one]
	rfl
	#align group_cohomology.resolution.d_eq groupCohomology.resolution.d_eq

Porting note: broken proof was #11039

Description

Examples

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions