Merge remote-tracking branch 'upstream/master' into bump/v4.29.0

Author: mathlib4-bot

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -1047,11 +1047,11 @@ def submonoidCongr (h : S = T) : S ≃* T :=
 -- this name is primed so that the version to `f.range` instead of `f.mrange` can be unprimed.
 /-- A monoid homomorphism `f : M →* N` with a left-inverse `g : N → M` defines a multiplicative
 equivalence between `M` and `f.mrange`.
-This is a bidirectional version of `MonoidHom.mrange_restrict`. -/
+This is a bidirectional version of `MonoidHom.mrangeRestrict`. -/
 @[to_additive (attr := simps +simpRhs)
   /-- An additive monoid homomorphism `f : M →+ N` with a left-inverse `g : N → M` defines an
   additive equivalence between `M` and `f.mrange`. This is a bidirectional version of
-  `AddMonoidHom.mrange_restrict`. -/]
+  `AddMonoidHom.mrangeRestrict`. -/]
 def ofLeftInverse' (f : M →* N) {g : N → M} (h : Function.LeftInverse g f) :
     M ≃* MonoidHom.mrange f :=
   { f.mrangeRestrict with

Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

@@ -1053,4 +1053,185 @@ lemma Scheme.exists_isOpenCover_and_isAffine [IsCofiltered I]
 
 end IsAffine
 
+section LocallyOfFinitePresentation
+
+include hc in
+/-- See `Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation` for the general case. -/
+private nonrec lemma Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation_of_isAffine
+    [IsCofiltered I] [LocallyOfFinitePresentation f]
+    [IsAffine S] [IsAffine X] [∀ i, IsAffine (D.obj i)]
+    (a : c.pt ⟶ X) (ha : c.π ≫ t = (Functor.const _).map (a ≫ f)) :
+    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i := by
+  -- Every scheme involved is affine, so the proof is merely translate to commutative algebra and
+  -- use `RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit`.
+  -- Unfortunately the translation takes 45 lines.
+  wlog hS : ∃ R, S = Spec R generalizing S
+  · obtain ⟨i, g, hg, hg'⟩ := this (t ≫ ((Functor.const I).mapIso S.isoSpec).hom)
+      (f ≫ S.isoSpec.hom) (by simp [reassoc_of% ha]) ⟨_, rfl⟩
+    exact ⟨i, g, hg, by simpa using congr($hg' ≫ S.isoSpec.inv)⟩
+  obtain ⟨R, rfl⟩ := hS
+  wlog hX : ∃ S, X = Spec S generalizing X
+  · obtain ⟨i, f, hf⟩ := this (a ≫ X.isoSpec.hom) (X.isoSpec.inv ≫ f)
+      (by simp [ha, - Functor.map_comp]) ⟨_, rfl⟩
+    exact ⟨i, f ≫ X.isoSpec.inv, by simpa [← Iso.comp_inv_eq] using hf⟩
+  obtain ⟨S, rfl⟩ := hX
+  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
+  wlog hD : ∃ D' : I ⥤ CommRingCatᵒᵖ, D = D' ⋙ Scheme.Spec generalizing D
+  · let e : D ⟶ D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
+    have inst (i) : IsIso (e.app i) := by dsimp [e]; infer_instance
+    have inst : IsIso e := NatIso.isIso_of_isIso_app e
+    have inst (i) : IsAffine ((D ⋙ Scheme.Γ.rightOp ⋙ Scheme.Spec).obj i) := by
+      dsimp; infer_instance
+    obtain ⟨i, g, hg, hg'⟩ := this _ _ ((IsLimit.postcomposeHomEquiv (asIso e) c).symm hc)
+      (inv e ≫ t) a (by simpa using ha) ⟨D ⋙ Scheme.Γ.rightOp, rfl⟩
+    exact ⟨i, e.app i ≫ g, by rwa [← Category.assoc], by simp [hg']⟩
+  obtain ⟨D, rfl⟩ := hD
+  let e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
+    NatIso.ofComponents (fun _ ↦ Iso.refl _) (by simp)
+  obtain ⟨t, rfl⟩ : ∃ t' : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp,
+      t = Functor.whiskerRight (NatTrans.rightOp t') Scheme.Spec ≫ e.hom :=
+    ⟨⟨fun i ↦ Spec.preimage (t.app i.unop), fun _ _ f ↦ Spec.map_injective
+      (by simpa using (t.naturality f.unop).symm)⟩, by ext : 2; simp [e]⟩
+  wlog hc' : ∃ c' : Cocone D.leftOp, c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c') generalizing c
+  · have inst : IsAffine c.pt := isAffine_of_isLimit _ hc
+    let e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
+    let c' := coneOfCoconeLeftOp ((Cocones.precompose e'.inv).obj (Γ.mapCocone c.op))
+    have inst : ∀ i, IsAffine ((D ⋙ Scheme.Spec).op.obj i).unop := by dsimp; infer_instance
+    obtain ⟨i, f, hf⟩ := this (Scheme.Spec.mapCone c') (isLimitOfPreserves _
+      (isLimitConeOfCoconeLeftOp _ ((IsColimit.precomposeHomEquiv e'.symm _).symm
+        (isColimitOfPreserves _ hc.op)))) (c.pt.isoSpec.inv ≫ a) (by
+        ext i
+        have : c.π.app i ≫ Spec.map (t.app (.op i)) = a ≫ Spec.map φ := by
+          simpa using congr((($ha).app i))
+        simp [c', e, e', ← this, Iso.eq_inv_comp, isoSpec_hom_naturality_assoc]) ⟨_, rfl⟩
+    refine ⟨i, f, ?_⟩
+    simpa [Iso.eq_inv_comp, c', isoSpec_hom_naturality_assoc, e'] using hf
+  obtain ⟨c', rfl⟩ := hc'
+  obtain ⟨ψ, rfl⟩ := Spec.map_surjective a
+  replace hc := isColimitOfConeOfCoconeLeftOp _ (isLimitOfReflects _ hc)
+  obtain ⟨i, g, hg, hg'⟩ :=
+    RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit _ D.leftOp t _ _ hc
+    (HasRingHomProperty.Spec_iff.mp ‹LocallyOfFinitePresentation (Spec.map φ)›) ψ fun i ↦ by
+    apply Spec.map_injective; simpa using congr(($ha).app i.unop).symm
+  exact ⟨i.unop, Spec.map g, by simpa using congr(Spec.map $hg').symm,
+    by simpa using congr(Spec.map $hg)⟩
+
+open TopologicalSpace in
+include hc in
+/--
+Given a cofiltered diagram of qcqs schemes `Dᵢ` over `S` with affine transition maps.
+If `X` is locally of finite presentation over `S`, then any `S`-morphism `lim Dᵢ ⟶ X` factors
+through some `lim Dᵢ ⟶ Dⱼ ⟶ X` for some `j`.
+-/
+lemma Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
+    [IsCofiltered I] [LocallyOfFinitePresentation f]
+    [∀ {i j} (f : i ⟶ j), IsAffineHom (D.map f)]
+    [∀ i, CompactSpace (D.obj i)] [∀ i, QuasiSeparatedSpace (D.obj i)]
+    (a : c.pt ⟶ X) (ha : c.π ≫ t = (Functor.const _).map (a ≫ f)) :
+    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i := by
+  classical
+  -- The open cover of `c := lim Dᵢ` indexed by triplets of affine opens `(U, V, W)` with
+  -- `U ⊆ c`, `V ⊆ X`, `W ⊆ S` such that `U` maps to `V` maps to `W`.
+  have 𝒰 := (c.pt.isBasis_affineOpens).isOpenCover_mem_and_le
+    (((X.isBasis_affineOpens).isOpenCover_mem_and_le
+    ((S.isBasis_affineOpens).isOpenCover.comap f.base.hom)).comap a.base.hom)
+  -- By qcqs, this cover descends to some finite affine open cover `𝒱` of `Dᵢ`.
+  obtain ⟨i, s, 𝒱, h𝒱, h𝒱𝒰⟩ := Scheme.exists_isOpenCover_and_isAffine D c hc _ 𝒰 fun U ↦ U.2.1
+  obtain ⟨i', fi'i, hi'⟩ : ∃ (i' : I) (fi'i : i' ⟶ i),
+      ∀ j, D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ j.1.1.2.1.2.1 := by
+    choose k fk hk using fun j ↦ exists_map_preimage_le_map_preimage D c hc (h𝒱𝒰 j).1.isCompact
+      (V := t.app i ⁻¹ᵁ j.1.1.2.1.2.1) (by
+      rw [← Hom.comp_preimage, ← NatTrans.comp_app, ha]
+      exact (h𝒱𝒰 j).2.symm.trans_le (j.1.prop.2.trans (a.preimage_mono j.1.1.2.prop.2)))
+    obtain ⟨i', fi'i, fi', hfi'⟩ := IsCofiltered.wideCospan fk
+    refine ⟨i', fi'i, fun j ↦ ?_⟩
+    rw [← hfi', Functor.map_comp, Hom.comp_preimage]
+    refine (Hom.preimage_mono _ (hk _)).trans ?_
+    simp only [← Hom.comp_preimage, t.naturality, Functor.const_obj_obj,
+      Functor.const_obj_map, Category.comp_id, le_refl]
+  -- Using the affine version `exists_π_app_comp_eq_of_locallyOfFinitePresentation_of_isAffine`,
+  -- one can now factor `Dⱼ ⁻¹ 𝒱ⱼ ⟶ lim Dᵢ ⟶ X` through some `Dⱼₖ ⁻¹ 𝒱ⱼ` for each `𝒱ⱼ`,
+  -- and by finite-ness we may chose a fixed `k` that works for every `j`.
+  have : ∃ k, ∃ (fk : k ⟶ i), ∀ j, ∃ (ak : ↑(D.map fk ⁻¹ᵁ 𝒱 j) ⟶ X),
+      ak ≫ f = Opens.ι _ ≫ t.app k ∧ c.π.app _ ∣_ _ ≫ ak = Opens.ι _ ≫ a := by
+    let 𝒱' := (D.map fi'i ⁻¹ᵁ 𝒱 ·)
+    have h𝒱'𝒰 (j : s) : c.π.app i' ⁻¹ᵁ 𝒱' j = j.1.1.1 := by
+      rw [← Hom.comp_preimage, c.w fi'i]; exact (h𝒱𝒰 j).2.symm
+    have _ (j k) : IsAffine ((opensDiagram D i' (𝒱' j)).obj k) := ((h𝒱𝒰 _).1.preimage _).preimage _
+    let t𝒱 (j : _) : opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj j.1.1.2.1.2 :=
+    { app k := (t.app k.left).resLE _ _ <| by
+        refine (Hom.preimage_mono _ (hi' _)).trans ?_
+        simp only [Functor.id_obj, Functor.const_obj_obj, ← Hom.comp_preimage, t.naturality,
+          Functor.const_obj_map, Category.comp_id, le_refl]
+      naturality {k₁ k₂} f₁₂ := by simp [Hom.resLE_comp_resLE] }
+    have (j : s) : IsAffine j.1.1.2.1.1 := j.1.1.2.prop.1
+    choose k ak hk hk' using fun j ↦ exists_π_app_comp_eq_of_locallyOfFinitePresentation_of_isAffine
+      _ (t𝒱 j) (f.resLE _ _ j.1.1.2.prop.2) _ (isLimitOpensCone D c hc i' (𝒱' j))
+      (a.resLE _ _ ((h𝒱'𝒰 _).trans_le j.1.prop.2)) (by
+      ext k
+      simp [t𝒱, Hom.resLE_comp_resLE, show c.π.app k.left ≫ t.app k.left = a ≫ f from
+        congr(($ha).app k.left)])
+    obtain ⟨i'', fi''i', fi'', hi''⟩ := IsCofiltered.wideCospan fun j ↦ (k j).hom
+    refine ⟨i'', fi''i' ≫ fi'i, fun j ↦
+      ⟨Scheme.homOfLE _ ?_ ≫ D.map (fi'' _) ∣_ _ ≫ ak j ≫ Opens.ι _, ?_, ?_⟩⟩
+    · simp only [← Hom.comp_preimage, ← Functor.map_comp, 𝒱', reassoc_of% hi'']; rfl
+    · have : ak j ≫ Opens.ι _ ≫ f = Opens.ι _ ≫ t.app (k j).left := by
+        simpa [t𝒱] using congr($(hk' j) ≫ Opens.ι _)
+      simp [this]
+    · have e : c.π.app i'' ⁻¹ᵁ D.map (fi''i' ≫ fi'i) ⁻¹ᵁ 𝒱 j ≤ c.π.app i' ⁻¹ᵁ 𝒱' j := by
+        simp only [← Hom.comp_preimage, Cone.w, 𝒱']; rfl
+      simpa [← AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict,
+        Scheme.Hom.resLE_comp_resLE_assoc] using congr(Scheme.homOfLE _ e ≫ $(hk j) ≫ Opens.ι _)
+  choose k fki ak hak hak' using this
+  -- We may then find an `l` for each `j₁` and `j₂` such that the map `Dⱼ₁ₗ ⁻¹ 𝒱ⱼ₁ ⟶ X` and
+  -- `Dⱼ₂ₗ ⁻¹ 𝒱ⱼ₂ ⟶ X` agrees on the intersection in `Dₗ`.
+  -- And again by finiteness we may choose a global `l`.
+  obtain ⟨l, flk, hl⟩ : ∃ (l : I) (flk : l ⟶ k), ∀ j₁ j₂, Scheme.homOfLE _ inf_le_left ≫
+      D.map flk ∣_ _ ≫ ak j₁ = Scheme.homOfLE _ inf_le_right ≫ D.map flk ∣_ _ ≫ ak j₂ := by
+    let 𝒱' := (D.map fki ⁻¹ᵁ 𝒱 ·)
+    have (j₁ j₂ : s) : ∃ (l : I) (flk : l ⟶ k), Scheme.homOfLE _ inf_le_left ≫ D.map flk ∣_ _ ≫
+        ak j₁ = Scheme.homOfLE _ inf_le_right ≫ D.map flk ∣_ _ ≫ ak j₂ := by
+      have _ (x) : CompactSpace ↥((opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).obj x) :=
+        isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ (𝒱' j₁ ⊓ 𝒱' j₂).isOpen
+          (((h𝒱𝒰 _).1.preimage _).isCompact.inter_of_isOpen ((h𝒱𝒰 _).1.preimage _).isCompact
+            (D.map fki ⁻¹ᵁ 𝒱 j₁).2 (D.map fki ⁻¹ᵁ 𝒱 j₂).2))
+      obtain ⟨⟨l, ⟨⟨⟩⟩, flk⟩, ⟨flk', ⟨⟨⟨⟩⟩⟩, h⟩, e⟩ :=
+        Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType _
+          (opensDiagramι .. ≫ (Over.forget k).whiskerLeft t) f _
+          (isLimitOpensCone D c hc k (𝒱' j₁ ⊓ 𝒱' j₂)) (i := .mk (𝟙 k))
+          (Scheme.homOfLE _ (by simp [𝒱']) ≫ ak j₁) (Scheme.homOfLE _ (by simp [𝒱']) ≫ ak j₂)
+          (by simp [hak]) (by simp [hak]) (by simp; simp [Hom.resLE, hak'])
+      obtain rfl : flk = flk' := by simpa using h.symm
+      refine ⟨l, flk, by simpa [← Scheme.Hom.resLE_eq_morphismRestrict] using e⟩
+    choose l flk hflk using this
+    obtain ⟨l', fl'k, fl'l, hl'⟩ := IsCofiltered.wideCospan (I := s × s) fun x ↦ flk x.1 x.2
+    refine ⟨l', fl'k, fun j₁ j₂ ↦ ?_⟩
+    have H : (D.map fl'k ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤
+        (D.map (fl'l (j₁, j₂)) ≫ D.map (flk j₁ j₂) ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) := by
+      simp only [← Functor.map_comp, reassoc_of% hl']; rfl
+    simpa [← Scheme.Hom.resLE_eq_morphismRestrict, Scheme.Hom.resLE_comp_resLE_assoc,
+      ← Functor.map_comp, hl'] using congr((D.map (fl'l (j₁, j₂))).resLE _ _ H ≫ $(hflk j₁ j₂))
+  -- We may glue the morphisms into `Dₗ ⟶ X` and verify that it indeed satisfies the hypothesis.
+  let h𝒲 := (h𝒱.comap (D.map fki).base.hom).comap (D.map flk).base.hom
+  let 𝒲 := Scheme.openCoverOfIsOpenCover _ (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 ·) h𝒲
+  let F := 𝒲.glueMorphisms (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) (fun j₁ j₂ ↦ by
+      rw [← cancel_epi (isPullback_opens_inf _ _).isoPullback.hom]
+      simpa [𝒲] using hl j₁ j₂)
+  have hF (j : s) : (D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ F = D.map flk ∣_ _ ≫ ak j :=
+    Scheme.Cover.ι_glueMorphisms ..
+  refine ⟨l, F, ?_, ?_⟩
+  · refine Cover.hom_ext (𝒲.pullback₁ (c.π.app l)) _ _ fun j ↦ ?_
+    rw [← cancel_epi (isPullback_morphismRestrict _ _).flip.isoPullback.hom]
+    dsimp [𝒲]
+    simp only [pullback.condition_assoc, IsPullback.isoPullback_hom_snd_assoc,
+      IsPullback.isoPullback_hom_fst_assoc, hF]
+    have h : c.π.app l ⁻¹ᵁ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j ≤ c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j := by
+      simp only [← Hom.comp_preimage, c.w_assoc, c.w]; rfl
+    simpa [← Scheme.Hom.resLE_eq_morphismRestrict, Scheme.Hom.resLE_comp_resLE_assoc] using
+      congr(Scheme.homOfLE _ h ≫ $(hak' j))
+  · refine 𝒲.hom_ext _ _ fun j ↦ ?_
+    simp [F, Cover.ι_glueMorphisms_assoc, hak]; rfl
+
+end LocallyOfFinitePresentation
+
 end AlgebraicGeometry

Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean

@@ -136,8 +136,8 @@ def mkOfHomFunctors (F : B → C) (F' : (a : B) → (b : B) → (a ⟶ b) ⥤ (F
 def id (B : Type u₁) [Bicategory.{w₁, v₁} B] : PrelaxFunctor B B where
   toPrelaxFunctorStruct := PrelaxFunctorStruct.id B
 
-instance : Inhabited (PrelaxFunctorStruct B B) :=
-  ⟨PrelaxFunctorStruct.id B⟩
+instance : Inhabited (PrelaxFunctor B B) :=
+  ⟨PrelaxFunctor.id B⟩
 
 variable (F : PrelaxFunctor B C)
 

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -551,6 +551,15 @@ theorem tulip {j₁ j₂ j₃ k₁ k₂ l : C} (f₁ : j₁ ⟶ k₁) (f₂ : j
   refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩ <;>
     simp only [hs₁, hs₂, Category.assoc]
 
+lemma wideSpan {I : Type*} [Finite I] {i : C} {j : I → C} (f : ∀ x, i ⟶ j x) :
+    ∃ k fik, ∃ g : ∀ x, j x ⟶ k, ∀ x, f x ≫ g x = fik := by
+  have : IsFiltered C := { nonempty := ⟨i⟩ }
+  classical
+  cases nonempty_fintype I
+  obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
+    (Finset.univ.image fun x ↦ ⟨i, j x, by simp, by simp, f x⟩)
+  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩
+
 end SpecialShapes
 
 end IsFiltered
@@ -849,6 +858,17 @@ omit [IsCofiltered C] in
 lemma iff_of_equivalence (e : C ≌ D) : IsCofiltered C ↔ IsCofiltered D :=
   ⟨fun _ ↦ .of_equivalence e, fun _ ↦ .of_equivalence e.symm⟩
 
+omit [IsCofiltered C] in
+lemma wideCospan [IsCofilteredOrEmpty C]
+    {I : Type*} [Finite I] {i : C} {j : I → C} (f : ∀ x, j x ⟶ i) :
+    ∃ k fki, ∃ g : ∀ x, k ⟶ j x, ∀ x, g x ≫ f x = fki := by
+  have : IsCofiltered C := { nonempty := ⟨i⟩ }
+  classical
+  cases nonempty_fintype I
+  obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
+    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)
+  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩
+
 end Nonempty
 
 

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

@@ -184,6 +184,26 @@ lemma GrpObj.one_inv : η[G] ≫ ι = η := by simp [GrpObj.inv_eq_inv, GrpObj.c
 
 @[deprecated (since := "2025-09-13")] alias Grp_Class.inv_eq_inv := GrpObj.inv_eq_inv
 
+/-- The commutator of `G` as a morphism. This is the map `(x, y) ↦ x * y * x⁻¹ * y⁻¹`,
+see `CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv`.
+This morphism is constant with value `1` if and only if `G` is commutative
+(see `CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η`). -/
+def GrpObj.commutator (G : C) [GrpObj G] : G ⊗ G ⟶ G :=
+  fst _ _ * snd _ _ * (fst _ _) ⁻¹ * (snd _ _) ⁻¹
+
+@[reassoc (attr := simp)]
+lemma GrpObj.lift_commutator_eq_mul_mul_inv_inv {X G : C} [GrpObj G] (f₁ f₂ : X ⟶ G) :
+    lift f₁ f₂ ≫ commutator G = f₁ * f₂ * f₁⁻¹ * f₂⁻¹ := by
+  simp [commutator, comp_mul, comp_inv]
+
+@[reassoc (attr := simp)]
+lemma GrpObj.η_whiskerRight_commutator : η ▷ G ≫ commutator G = toUnit _ ≫ η := by
+  simp [commutator, comp_mul, comp_inv, one_eq_one]
+
+@[reassoc (attr := simp)]
+lemma GrpObj.whiskerLeft_η_commutator : G ◁ η ≫ commutator G = toUnit _ ≫ η := by
+  simp [commutator, comp_mul, comp_inv, one_eq_one]
+
 variable [BraidedCategory C]
 
 instance [IsCommMonObj G] : IsMonHom ι[G] where
@@ -243,4 +263,17 @@ abbrev Hom.commGroup [IsCommMonObj G] : CommGroup (X ⟶ G) where
 
 scoped[CategoryTheory.MonObj] attribute [instance] Hom.commGroup
 
+section
+
+/-- `G` is a commutative group object if and only if the commutator map `(x, y) ↦ x * y * x⁻¹ * y⁻¹`
+is constant. -/
+lemma isCommMonObj_iff_commutator_eq_toUnit_η :
+    IsCommMonObj G ↔ GrpObj.commutator G = toUnit _ ≫ η := by
+  rw [isCommMonObj_iff_isMulCommutative]
+  refine ⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩
+  · simp [GrpObj.commutator, one_eq_one]
+  · simpa [one_eq_one, mul_inv_eq_iff_eq_mul] using congr(lift f g ≫ $heq)
+
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

@@ -385,4 +385,10 @@ def mulEquivCongrRight (e : M ≅ N) [IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (
   ((yonedaMon.mapIso <| Mon.mkIso' e).app <| .op X).monCatIsoToMulEquiv
 
 end Hom
+
+/-- A monoid object `M` is commutative if and only if `X ⟶ M` is commutative for all `X`. -/
+lemma isCommMonObj_iff_isMulCommutative (M : C) [MonObj M] [BraidedCategory C] :
+    IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M) := by
+  exact ⟨fun h X ↦ ⟨⟨by simp [mul_comm]⟩⟩, fun h ↦ ⟨by simp [mul_eq_mul, comp_mul, mul_comm]⟩⟩
+
 end CategoryTheory

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -638,6 +638,9 @@ theorem mk_subtype_le_of_subset {α : Type u} {p q : α → Prop} (h : ∀ ⦃x
 theorem mk_le_mk_of_subset {α} {s t : Set α} (h : s ⊆ t) : #s ≤ #t :=
   ⟨Set.embeddingOfSubset s t h⟩
 
+theorem mk_monotone : Monotone (α := Set α) (mk ∘ (↑)) :=
+  fun _ _ ↦ mk_le_mk_of_subset
+
 @[deprecated mk_eq_zero (since := "2026-01-31")]
 theorem mk_emptyCollection (α : Type u) : #(∅ : Set α) = 0 :=
   mk_eq_zero _
@@ -854,6 +857,12 @@ lemma card_lt_card_of_left_finite {A B : Set α} (hfin : A.Finite) (hlt : A ⊂
   · exact card_lt_card_of_right_finite hfin hlt
   · exact (lt_aleph0_iff_subtype_finite.mpr hfin).trans_le <| Cardinal.aleph0_le_mk_iff.mpr hinf
 
+theorem mk_strictMono [Finite α] : StrictMono (α := Set α) (mk ∘ (↑)) :=
+  fun _ s ↦ card_lt_card_of_right_finite s.toFinite
+
+theorem mk_strictMonoOn : StrictMonoOn (mk ∘ (↑)) {s : Set α | s.Finite} :=
+  fun _ _ _ ↦ card_lt_card_of_right_finite
+
 theorem le_mk_diff_add_mk (S T : Set α) : #S ≤ #(S \ T : Set α) + #T :=
   (mk_le_mk_of_subset <| subset_diff_union _ _).trans <| mk_union_le _ _
 

Mathlib/Topology/Sets/OpenCover.lean

@@ -63,6 +63,21 @@ lemma isTopologicalBasis (hu : IsOpenCover u)
 
 end IsOpenCover
 
+lemma Opens.IsBasis.isOpenCover {S : Set (Opens X)} (hS : Opens.IsBasis S) :
+    IsOpenCover (fun U : S ↦ (U : Opens X)) :=
+  top_le_iff.mp (subset_trans hS.2.superset (by simp))
+
+/-- Given an open cover and a basis,
+the set of basis elements contained in any of the covers is still a cover. -/
+lemma Opens.IsBasis.isOpenCover_mem_and_le {S : Set (Opens X)} (hS : Opens.IsBasis S)
+    {U : ι → Opens X} (hU : IsOpenCover U) :
+    IsOpenCover (fun V : { x : Opens X × ι // x.1 ∈ S ∧ x.1 ≤ U x.2 } ↦ V.1.1) := by
+  refine top_le_iff.mp fun x _ ↦ ?_
+  obtain ⟨i, hxi⟩ := hU.exists_mem x
+  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2
+  simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]
+  exact ⟨⟨(V, i), hV, hVU⟩, hxV⟩
+
 end TopologicalSpace
 
 section Irreducible