Trigger CI for leanprover/lean4#2648

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Hom.Iterate
 import Mathlib.Algebra.Hom.NonUnitalAlg
 import Mathlib.LinearAlgebra.TensorProduct
@@ -152,7 +153,18 @@ end NonUnital
 
 section Semiring
 
-variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
+variable (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+
+variable {R A B} in
+/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
+equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various
+specialized `ext` lemmas about `→ₗ[R]` to then be applied.
+
+This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/
+theorem map_mul_iff (f : A →ₗ[R] B) :
+    (∀ x y, f (x * y) = f x * f y) ↔
+      (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f :=
+  Iff.symm LinearMap.ext_iff₂
 
 /-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
 the algebra.

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -32,12 +32,12 @@ typeclass instead.
 There are many similarly-named definitions elsewhere which do not refer to this type alias. These
 refer to restricting the scalar type in a bundled type, such as from `A →ₗ[R] B` to `A →ₗ[S] B`:
 
-* `LinearMap.RestrictScalars`
-* `LinearEquiv.RestrictScalars`
-* `AlgHom.RestrictScalars`
-* `AlgEquiv.RestrictScalars`
-* `Submodule.RestrictScalars`
-* `Subalgebra.RestrictScalars`
+* `LinearMap.restrictScalars`
+* `LinearEquiv.restrictScalars`
+* `AlgHom.restrictScalars`
+* `AlgEquiv.restrictScalars`
+* `Submodule.restrictScalars`
+* `Subalgebra.restrictScalars`
 -/
 
 
@@ -214,7 +214,7 @@ theorem RestrictScalars.ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) :
 #align restrict_scalars.ring_equiv_map_smul RestrictScalars.ringEquiv_map_smul
 
 /-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
-instance : Algebra R (RestrictScalars R S A) :=
+instance RestrictScalars.algebra : Algebra R (RestrictScalars R S A) :=
   { (algebraMap S A).comp (algebraMap R S) with
     smul := (· • ·)
     commutes' := fun _ _ ↦ Algebra.commutes' _ _

Mathlib/Algebra/DirectSum/Algebra.lean

@@ -114,12 +114,14 @@ coercions such as `Submodule.subtype (A i)`, and the `[GMonoid A]` structure ori
 can be discharged by `rfl`. -/
 @[simps]
 def toAlgebra (f : ∀ i, A i →ₗ[R] B) (hone : f _ GradedMonoid.GOne.one = 1)
-    (hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (GradedMonoid.GMul.mul ai aj) = f _ ai * f _ aj)
-    (hcommutes : ∀ r, (f 0) (GAlgebra.toFun r) = (algebraMap R B) r) : (⨁ i, A i) →ₐ[R] B :=
-  { toSemiring (fun i => (f i).toAddMonoidHom) hone
-      @hmul with
+    (hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (GradedMonoid.GMul.mul ai aj) = f _ ai * f _ aj) :
+    (⨁ i, A i) →ₐ[R] B :=
+  { toSemiring (fun i => (f i).toAddMonoidHom) hone @hmul with
     toFun := toSemiring (fun i => (f i).toAddMonoidHom) hone @hmul
-    commutes' := fun r => (DirectSum.toSemiring_of _ hone hmul _ _).trans (hcommutes r) }
+    commutes' := fun r => by
+      show toModule R _ _ f (algebraMap R _ r) = _
+      rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
+        ←lof_eq_of R, toModule_lof, hone] }
 #align direct_sum.to_algebra DirectSum.toAlgebra
 
 /-- Two `AlgHom`s out of a direct sum are equal if they agree on the generators.

Mathlib/Algebra/DirectSum/Internal.lean

@@ -317,7 +317,7 @@ end Submodule
 /-- The canonical algebra isomorphism between `⨁ i, A i` and `R`. -/
 def DirectSum.coeAlgHom [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R]
     (A : ι → Submodule S R) [SetLike.GradedMonoid A] : (⨁ i, A i) →ₐ[S] R :=
-  DirectSum.toAlgebra S _ (fun i => (A i).subtype) rfl (fun _ _ => rfl) fun _ => rfl
+  DirectSum.toAlgebra S _ (fun i => (A i).subtype) rfl (fun _ _ => rfl)
 #align direct_sum.coe_alg_hom DirectSum.coeAlgHom
 
 /-- The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of

Mathlib/Algebra/GroupPower/Order.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.group_power.order from "leanprover-community/mathlib"@"00f91228655eecdcd3ac97a7fd8dbcb139fe990a"
 
@@ -501,6 +502,9 @@ theorem self_lt_pow (h : 1 < a) (h2 : 1 < m) : a < a ^ m := by
     a = a ^ 1 := (pow_one _).symm
     _ < a ^ m := pow_lt_pow h h2
 
+theorem self_le_pow (h : 1 ≤ a) (h2 : 1 ≤ m) : a ≤ a ^ m :=
+  le_self_pow h <| Nat.one_le_iff_ne_zero.mp h2
+
 theorem strictAnti_pow (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun n : ℕ => a ^ n :=
   strictAnti_nat_of_succ_lt fun n => by
     simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one

Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

@@ -17,7 +17,9 @@ This typeclass is named `[F.PreservesHomology]`, and is automatically
 satisfied when `F` preserves both finite limits and finite colimits.
 
 If `S : ShortComplex C` and `[F.PreservesHomology]`, then there is an
-isomorphism `S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology`.
+isomorphism `S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology`, which
+is part of the natural isomorphism `homologyFunctorIso F` between the functors
+`F.mapShortComplex ⋙ homologyFunctor D` and `homologyFunctor C ⋙ F`.
 
 -/
 
@@ -518,8 +520,206 @@ lemma mapLeftHomologyIso_inv_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomo
   rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc,
     Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
 
+@[reassoc]
+lemma mapOpcyclesIso_hom_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    opcyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapOpcyclesIso F).hom =
+      (S₁.mapOpcyclesIso F).hom ≫ F.map (opcyclesMap φ) := by
+  dsimp only [opcyclesMap, mapOpcyclesIso, RightHomologyData.opcyclesIso,
+    opcyclesMapIso', Iso.refl]
+  simp only [RightHomologyData.map_opcyclesMap', Functor.mapShortComplex_obj, ← opcyclesMap'_comp,
+    comp_id, id_comp]
+
+@[reassoc]
+lemma mapOpcyclesIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv =
+      (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ) := by
+  rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc,
+    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
+
+@[reassoc]
+lemma mapRightHomologyIso_hom_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom =
+      (S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ) := by
+  dsimp only [rightHomologyMap, mapRightHomologyIso, RightHomologyData.rightHomologyIso,
+    rightHomologyMapIso', Iso.refl]
+  simp only [RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
+    ← rightHomologyMap'_comp, comp_id, id_comp]
+
+@[reassoc]
+lemma mapRightHomologyIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
+      (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ) := by
+  rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_hom_naturality_assoc,
+    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
+
+@[reassoc]
+lemma mapHomologyIso_hom_naturality [S₁.HasHomology] [S₂.HasHomology]
+    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
+    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
+    @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ ≫
+      (S₂.mapHomologyIso F).hom = (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ) := by
+  dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
+    LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
+    Iso.symm, Iso.trans, Iso.refl]
+  simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]
+
+@[reassoc]
+lemma mapHomologyIso_inv_naturality [S₁.HasHomology] [S₂.HasHomology]
+    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
+    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
+    F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv =
+      (S₁.mapHomologyIso F).inv ≫
+      @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ := by
+  rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_hom_naturality_assoc,
+    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
+
+@[reassoc]
+lemma mapHomologyIso'_hom_naturality [S₁.HasHomology] [S₂.HasHomology]
+    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ ≫
+      (S₂.mapHomologyIso' F).hom = (S₁.mapHomologyIso' F).hom ≫ F.map (homologyMap φ) := by
+  dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']
+  simp only [← RightHomologyData.rightHomologyIso_hom_naturality_assoc _
+    ((homologyData S₁).right.map F) ((homologyData S₂).right.map F), assoc,
+    ← RightHomologyData.map_rightHomologyMap', ← F.map_comp,
+    RightHomologyData.rightHomologyIso_inv_naturality _
+      (homologyData S₁).right (homologyData S₂).right]
+
+@[reassoc]
+lemma mapHomologyIso'_inv_naturality [S₁.HasHomology] [S₂.HasHomology]
+    [(S₁.map F).HasHomology] [(S₂.map F).HasHomology]
+    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
+    F.map (homologyMap φ) ≫ (S₂.mapHomologyIso' F).inv = (S₁.mapHomologyIso' F).inv ≫
+      @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ := by
+  rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc,
+    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
+
+variable (S)
+
+lemma mapHomologyIso'_eq_mapHomologyIso [S.HasHomology] [F.PreservesLeftHomologyOf S]
+    [F.PreservesRightHomologyOf S] :
+    S.mapHomologyIso' F = S.mapHomologyIso F := by
+  ext
+  rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]
+  dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso,
+    rightHomologyIso, RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso,
+    leftHomologyIso, LeftHomologyData.leftHomologyIso]
+  simp only [RightHomologyData.map_H, rightHomologyMapIso'_inv, rightHomologyMapIso'_hom, assoc,
+    Functor.map_comp, RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
+    Functor.map_id, LeftHomologyData.map_H, leftHomologyMapIso'_inv, leftHomologyMapIso'_hom,
+    LeftHomologyData.map_leftHomologyMap', ← rightHomologyMap'_comp_assoc, ← leftHomologyMap'_comp,
+    ← leftHomologyMap'_comp_assoc, id_comp]
+  have γ : HomologyMapData (𝟙 (S.map F)) (map S F).homologyData (S.homologyData.map F) := default
+  have eq := γ.comm
+  rw [← γ.left.leftHomologyMap'_eq, ← γ.right.rightHomologyMap'_eq] at eq
+  dsimp at eq
+  simp only [← reassoc_of% eq, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]
+
 end
 
+section
+
+variable {S}
+  {F G : C ⥤ D} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms]
+  [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S]
+  [F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S]
+
+/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
+the left homology of a short complex `S`, and a left homology data for `S`,
+this is the left homology map data for the morphism `S.mapNatTrans τ`
+obtained by evaluating `τ`. -/
+@[simps]
+def LeftHomologyMapData.natTransApp (h : LeftHomologyData S) (τ : F ⟶ G) :
+    LeftHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G) where
+  φK := τ.app h.K
+  φH := τ.app h.H
+
+/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
+the right homology of a short complex `S`, and a right homology data for `S`,
+this is the right homology map data for the morphism `S.mapNatTrans τ`
+obtained by evaluating `τ`. -/
+@[simps]
+def RightHomologyMapData.natTransApp (h : RightHomologyData S) (τ : F ⟶ G) :
+    RightHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G) where
+  φQ := τ.app h.Q
+  φH := τ.app h.H
+
+/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
+the homology of a short complex `S`, and a homology data for `S`,
+this is the homology map data for the morphism `S.mapNatTrans τ`
+obtained by evaluating `τ`. -/
+@[simps]
+def HomologyMapData.natTransApp (h : HomologyData S) (τ : F ⟶ G) :
+    HomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G) where
+  left := LeftHomologyMapData.natTransApp h.left τ
+  right := RightHomologyMapData.natTransApp h.right τ
+
+variable (S)
+
+lemma homologyMap_mapNatTrans [S.HasHomology] (τ : F ⟶ G) :
+    homologyMap (S.mapNatTrans τ) =
+      (S.mapHomologyIso F).hom ≫ τ.app S.homology ≫ (S.mapHomologyIso G).inv :=
+  (LeftHomologyMapData.natTransApp S.homologyData.left τ).homologyMap_eq
+
+end
+
+section
+
+variable [HasKernels C] [HasCokernels C] [HasKernels D] [HasCokernels D]
+
+/-- The natural isomorphism
+`F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F`
+for a functor `F : C ⥤ D` which preserves homology. --/
+noncomputable def cyclesFunctorIso [F.PreservesHomology] :
+    F.mapShortComplex ⋙ ShortComplex.cyclesFunctor D ≅
+      ShortComplex.cyclesFunctor C ⋙ F :=
+  NatIso.ofComponents (fun S => S.mapCyclesIso F)
+    (fun f => ShortComplex.mapCyclesIso_hom_naturality f F)
+
+/-- The natural isomorphism
+`F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F`
+for a functor `F : C ⥤ D` which preserves homology. --/
+noncomputable def leftHomologyFunctorIso [F.PreservesHomology] :
+    F.mapShortComplex ⋙ ShortComplex.leftHomologyFunctor D ≅
+      ShortComplex.leftHomologyFunctor C ⋙ F :=
+  NatIso.ofComponents (fun S => S.mapLeftHomologyIso F)
+    (fun f => ShortComplex.mapLeftHomologyIso_hom_naturality f F)
+
+/-- The natural isomorphism
+`F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F`
+for a functor `F : C ⥤ D` which preserves homology. --/
+noncomputable def opcyclesFunctorIso [F.PreservesHomology] :
+    F.mapShortComplex ⋙ ShortComplex.opcyclesFunctor D ≅
+      ShortComplex.opcyclesFunctor C ⋙ F :=
+  NatIso.ofComponents (fun S => S.mapOpcyclesIso F)
+    (fun f => ShortComplex.mapOpcyclesIso_hom_naturality f F)
+
+/-- The natural isomorphism
+`F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F`
+for a functor `F : C ⥤ D` which preserves homology. --/
+noncomputable def rightHomologyFunctorIso [F.PreservesHomology] :
+    F.mapShortComplex ⋙ ShortComplex.rightHomologyFunctor D ≅
+      ShortComplex.rightHomologyFunctor C ⋙ F :=
+  NatIso.ofComponents (fun S => S.mapRightHomologyIso F)
+    (fun f => ShortComplex.mapRightHomologyIso_hom_naturality f F)
+
+end
+
+/-- The natural isomorphism
+`F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F`
+for a functor `F : C ⥤ D` which preserves homology. --/
+noncomputable def homologyFunctorIso
+    [CategoryWithHomology C] [CategoryWithHomology D] [F.PreservesHomology] :
+    F.mapShortComplex ⋙ ShortComplex.homologyFunctor D ≅
+      ShortComplex.homologyFunctor C ⋙ F :=
+  NatIso.ofComponents (fun S => S.mapHomologyIso F)
+    (fun f => ShortComplex.mapHomologyIso_hom_naturality f F)
+
 end ShortComplex
 
 end CategoryTheory