Skip to content

[Merged by Bors] - chore: classify broken proof was porting notes #11040

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
pitmonticone wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: classify broken proof was porting notes #11040

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ and the homogeneous `linearYonedaObjResolution`. -/
(linearYonedaObjResolution A).d n (n + 1) ≫
(diagonalHomEquiv (n + 1) A).toModuleIso.hom := by
ext f g
/- Porting note: broken proof was
/- 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,
Expand Down Expand Up @@ -183,7 +183,7 @@ 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: broken proof was
/- 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
Expand Down
20 changes: 10 additions & 10 deletions Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ theorem actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin (
induction' n with n hn
· exact Prod.ext rfl (funext fun x => Fin.elim0 x)
· refine' Prod.ext rfl (funext fun x => _)
/- Porting note: broken proof was
/- 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,
Expand All @@ -134,7 +134,7 @@ theorem actionDiagonalSucc_inv_apply {G : Type u} [Group G] {n : ℕ} (g : G) (f
simp only [Subsingleton.elim x 0, Pi.smul_apply, Fin.partialProd_zero, smul_eq_mul, mul_one]
rfl
· intro g
/- Porting note: broken proof was
/- 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,
Expand Down Expand Up @@ -176,7 +176,7 @@ variable {k G n}
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: broken proof was
/- 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,
Expand All @@ -200,7 +200,7 @@ theorem diagonalSucc_hom_single (f : Gⁿ⁺¹) (a : k) :
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: broken proof was
/- 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,
Expand All @@ -222,7 +222,7 @@ 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: broken proof was
/- 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,
Expand All @@ -244,7 +244,7 @@ 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: broken proof was
/- 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,
Expand Down Expand Up @@ -279,7 +279,7 @@ def ofMulActionBasisAux :
-- 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: broken proof was
/- 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']
Expand Down Expand Up @@ -340,7 +340,7 @@ 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: broken proof was
/- 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,
Expand All @@ -361,7 +361,7 @@ theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1)
((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: broken proof was
/- 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,
Expand Down Expand Up @@ -555,7 +555,7 @@ set_option linter.uppercaseLean3 false in
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: broken proof was
/- 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,
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RepresentationTheory/Rep.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,7 @@ set_option linter.uppercaseLean3 false in
@[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: broken proof was
-- 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 _ _-/
Expand Down