From 0f0a217d5d731dad8a22f3f7095634784d30ac14 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Fri, 31 Jul 2026 08:20:33 +0000 Subject: [PATCH 01/14] chore(CategoryTheory): remove `backward` options using `implicit_reducible` (#42161) This PR removes a lot of the transparency related `set_option`. I did this by using `#defeq_abuse in` to determine which definition was not being unfolded, and then tagging such definitions with `implicit_reducible`. In particular `backward.isDefEq.respectTransparency` can almost always be removed like this, but `backward.defeqAttrib.useBackward` is still sometimes tricky to remove. Presumably, the changes from this PR will let us remove many more `set_option` in further files that this PR doesn't touch. --- Mathlib/CategoryTheory/Adjunction/Basic.lean | 13 +--- Mathlib/CategoryTheory/Comma/Basic.lean | 26 +------ Mathlib/CategoryTheory/EqToHom.lean | 2 - Mathlib/CategoryTheory/Equivalence.lean | 25 ++----- Mathlib/CategoryTheory/EssentialImage.lean | 8 +- Mathlib/CategoryTheory/Functor/Category.lean | 2 - .../CategoryTheory/Functor/FullyFaithful.lean | 3 - Mathlib/CategoryTheory/Limits/Cones.lean | 75 +++++-------------- Mathlib/CategoryTheory/Limits/HasLimits.lean | 35 --------- Mathlib/CategoryTheory/Limits/IsLimit.lean | 28 +------ .../Limits/Shapes/Equalizers.lean | 44 ++--------- .../Limits/Shapes/IsTerminal.lean | 32 ++------ .../Limits/Shapes/Products.lean | 55 +------------- .../Limits/Shapes/Terminal.lean | 13 ---- Mathlib/CategoryTheory/NatIso.lean | 2 +- Mathlib/CategoryTheory/Opposites.lean | 75 ++++--------------- Mathlib/CategoryTheory/Whiskering.lean | 39 ++-------- 17 files changed, 74 insertions(+), 403 deletions(-) diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean index f0e132087a6..fb5b3de90eb 100644 --- a/Mathlib/CategoryTheory/Adjunction/Basic.lean +++ b/Mathlib/CategoryTheory/Adjunction/Basic.lean @@ -79,8 +79,6 @@ Conversely `Equivalence.toAdjunction` recovers the underlying adjunction from an isomorphism `L ⋙ R ≅ 𝟭 C`, the unit is an isomorphism, and similarly for the counit. -/ -set_option backward.defeqAttrib.useBackward true - @[expose] public section namespace CategoryTheory @@ -314,7 +312,6 @@ def corepresentableBy (X : C) : homEquiv := adj.homEquiv _ _ homEquiv_comp := by simp -set_option backward.isDefEq.respectTransparency false in /-- If `adj : F ⊣ G`, and `Y : D`, then `G.obj Y` represents `X ↦ (F.obj X ⟶ Y)`. -/ @[simps] def representableBy (Y : D) : @@ -538,7 +535,6 @@ lemma homEquiv_ofNatIsoRight_symm_apply {F : C ⥤ D} {G H : D ⥤ C} (adj : F (adj.homEquiv _ _).symm (f ≫ iso.inv.app _) := by simp -set_option backward.isDefEq.respectTransparency.types false in /-- The isomorphism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that `Adjunction.homEquiv` is natural in both arguments. -/ @[simps!] @@ -547,7 +543,6 @@ def compYonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category. G ⋙ yoneda ≅ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op := NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv Y.unop X).toIso.symm -set_option backward.isDefEq.respectTransparency.types false in /-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that `Adjunction.homEquiv` is natural in both arguments. -/ @[simps!] @@ -556,7 +551,7 @@ def compCoyonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Categor F.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft _ _ _).obj G := NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv X.unop Y).toIso -set_option backward.isDefEq.respectTransparency.types false in +set_option backward.defeqAttrib.useBackward true in /-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ uliftCoyoneda`. This states that `Adjunction.homEquiv` is natural in both arguments. -/ @[simps!] @@ -611,7 +606,7 @@ variable (e : ∀ X Y, (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) a bijection `e` between `F_obj X ⟶ Y` and `X ⟶ G.obj Y` satisfying a naturality law `he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g`. Dual to `rightAdjointOfEquiv`. -/ -@[simps!] +@[implicit_reducible, simps!] def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) : C ⥤ D where obj := F_obj map {X} {X'} f := (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _)) @@ -624,7 +619,6 @@ def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.ma variable (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) -set_option backward.isDefEq.respectTransparency false in /-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual to `adjunctionOfEquivRight`. -/ @[simps!] @@ -653,7 +647,7 @@ private theorem he'' (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law `he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g`. Dual to `leftAdjointOfEquiv`. -/ -@[simps!] +@[implicit_reducible, simps!] def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : D ⥤ C where obj := G_obj map {Y} {Y'} g := (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g) @@ -664,7 +658,6 @@ def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply] simp -set_option backward.isDefEq.respectTransparency false in /-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual to `adjunctionOfEquivLeft`. -/ @[simps!] diff --git a/Mathlib/CategoryTheory/Comma/Basic.lean b/Mathlib/CategoryTheory/Comma/Basic.lean index 70748bb0d45..8a3cde979b9 100644 --- a/Mathlib/CategoryTheory/Comma/Basic.lean +++ b/Mathlib/CategoryTheory/Comma/Basic.lean @@ -265,7 +265,6 @@ attribute [to_dual existing] map_obj_left attribute [to_dual existing (reorder := A B, 2 4, A' B', 8 10, L R, L' R', F₁ F₂, α β, X Y)] map_map_left -set_option backward.isDefEq.respectTransparency false in @[to_dual existing (reorder := A B, 2 4, A' B', 8 10, L R, L' R', F₁ F₂, α β) map_obj_hom] theorem map_obj_hom' (X : Comma L R) : ((map α β).obj X).hom = (α.app X.left ≫ F.map X.hom) ≫ β.app X.right := by simp @@ -277,7 +276,6 @@ instance faithful_map [F₁.Faithful] [F₂.Faithful] : (map α β).Faithful whe · exact F₁.map_injective (congr_arg CommaMorphism.left h) · exact F₂.map_injective (congr_arg CommaMorphism.right h) -set_option backward.isDefEq.respectTransparency false in @[to_dual self (reorder := A B, 2 4, A' B', 8 10, L R, L' R', F₁ F₂, α β, 23 24, 25 26)] instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (map α β).Full where map_surjective {X Y} φ := @@ -349,8 +347,6 @@ def mapLeft (l : L₁ ⟶ L₂) : Comma L₂ R ⥤ Comma L₁ R where attribute [to_dual existing] mapLeft_map_left attribute [to_dual existing] mapLeft_map_right -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in set_option linter.translate.warnInvalid false in /-- The functor `Comma L R ⥤ Comma L R` induced by the identity natural transformation on `L` is naturally isomorphic to the identity functor. -/ @@ -360,8 +356,6 @@ naturally isomorphic to the identity functor. -/] def mapLeftId : mapLeft R (𝟙 L) ≅ 𝟭 _ := NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _)) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in set_option linter.translate.warnInvalid false in /-- The functor `Comma L₁ R ⥤ Comma L₃ R` induced by the composition of two natural transformations `l : L₁ ⟶ L₂` and `l' : L₂ ⟶ L₃` is naturally isomorphic to the composition of the two functors @@ -383,7 +377,6 @@ set_option linter.translate.warnInvalid false in def mapLeftEq (l l' : L₁ ⟶ L₂) (h : l = l') : mapLeft R l ≅ mapLeft R l' := NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _)) -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in set_option linter.translate.warnInvalid false in /-- A natural isomorphism `L₁ ≅ L₂` induces an equivalence of categories @@ -417,7 +410,6 @@ def preLeft (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) : Comma (F ⋙ L) R ⥤ Co right := f.right w := by simpa using! f.w } -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- `Comma.preLeft` is a particular case of `Comma.map`, but with better definitional properties. -/ @@ -445,9 +437,8 @@ instance (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.EssSurj] : (preLeft F L R) instance isEquivalence_preLeft (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.IsEquivalence] : (preLeft F L R).IsEquivalence where -set_option backward.isDefEq.respectTransparency false in /-- The functor `(L, R) ⥤ (L ⋙ F, R ⋙ F)` -/ -@[to_dual self, simps] +@[implicit_reducible, to_dual self, simps] def post (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : Comma L R ⥤ Comma (L ⋙ F) (R ⋙ F) where obj X := { left := X.left @@ -461,8 +452,6 @@ def post (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : Comma L R ⥤ Comma (L ⋙ attribute [to_dual existing] post_obj_left attribute [to_dual self] post_obj_hom -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- `Comma.post` is a particular case of `Comma.map`, but with better definitional properties. -/ @[to_dual self] def postIso (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : @@ -488,7 +477,7 @@ instance isEquivalence_post (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.IsEquiv /-- The canonical functor from the product of two categories to the comma category of their respective functors into `Discrete PUnit`. -/ -@[simps] +@[implicit_reducible, simps] def fromProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : A × B ⥤ Comma L R where obj X := @@ -499,7 +488,6 @@ def fromProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : { left := f.1 right := f.2 } -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- Taking the comma category of two functors into `Discrete PUnit` results in something is equivalent to their product. -/ @@ -511,28 +499,24 @@ def equivProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : unitIso := Iso.refl _ counitIso := Iso.refl _ -set_option backward.isDefEq.respectTransparency.types false in /-- Taking the comma category of a functor into `A ⥤ Discrete PUnit` and the identity `Discrete PUnit ⥤ Discrete PUnit` results in a category equivalent to `A`. -/ def toPUnitIdEquiv (L : A ⥤ Discrete PUnit) (R : Discrete PUnit ⥤ Discrete PUnit) : Comma L R ≌ A := (equivProd L _).trans (prod.rightUnitorEquivalence A) -set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem toPUnitIdEquiv_functor_iso {L : A ⥤ Discrete PUnit} {R : Discrete PUnit ⥤ Discrete PUnit} : (toPUnitIdEquiv L R).functor = fst L R := rfl -set_option backward.isDefEq.respectTransparency.types false in /-- Taking the comma category of the identity `Discrete PUnit ⥤ Discrete PUnit` and a functor `B ⥤ Discrete PUnit` results in a category equivalent to `B`. -/ def toIdPUnitEquiv (L : Discrete PUnit ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : Comma L R ≌ B := (equivProd _ R).trans (prod.leftUnitorEquivalence B) -set_option backward.isDefEq.respectTransparency.types false in @[simp] theorem toIdPUnitEquiv_functor_iso {L : Discrete PUnit ⥤ Discrete PUnit} {R : B ⥤ Discrete PUnit} : @@ -547,7 +531,7 @@ open Opposite set_option backward.defeqAttrib.useBackward true in /-- The canonical functor from `Comma L R` to `(Comma R.op L.op)ᵒᵖ`. -/ -@[simps] +@[implicit_reducible, simps] def opFunctor : Comma L R ⥤ (Comma R.op L.op)ᵒᵖ where obj X := ⟨op X.right, op X.left, op X.hom⟩ map f := ⟨op f.right, op f.left, Quiver.Hom.unop_inj (by simp)⟩ @@ -565,7 +549,7 @@ def opFunctorCompSnd : (opFunctor L R).leftOp ⋙ snd _ _ ≅ (fst _ _).op := Iso.refl _ /-- The canonical functor from `Comma L.op R.op` to `(Comma R L)ᵒᵖ`. -/ -@[simps] +@[implicit_reducible, simps] def unopFunctor : Comma L.op R.op ⥤ (Comma R L)ᵒᵖ where obj X := ⟨X.right.unop, X.left.unop, X.hom.unop⟩ map f := ⟨f.right.unop, f.left.unop, Quiver.Hom.op_inj (by simpa using! f.w.symm)⟩ @@ -580,8 +564,6 @@ def unopFunctorCompFst : unopFunctor L R ⋙ (fst _ _).op ≅ snd _ _ := def unopFunctorCompSnd : unopFunctor L R ⋙ (snd _ _).op ≅ fst _ _ := Iso.refl _ -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The canonical equivalence between `Comma L R` and `(Comma R.op L.op)ᵒᵖ`. -/ @[simps] def opEquiv : Comma L R ≌ (Comma R.op L.op)ᵒᵖ where diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean index 8af05f699ff..fba7c0c44b2 100644 --- a/Mathlib/CategoryTheory/EqToHom.lean +++ b/Mathlib/CategoryTheory/EqToHom.lean @@ -390,8 +390,6 @@ lemma ObjectProperty.eqToHom_hom {C : Type*} [Category C] {P : ObjectProperty C} subst h rfl -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- If `T ≃ D` is a bijection and `D` is a category, then `InducedCategory D e` is equivalent to `D`. -/ @[simps] diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean index 24f7948bf55..a1c1e527f13 100644 --- a/Mathlib/CategoryTheory/Equivalence.lean +++ b/Mathlib/CategoryTheory/Equivalence.lean @@ -57,8 +57,6 @@ if it is full, faithful and essentially surjective. We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bundled equivalence. -/ -set_option backward.defeqAttrib.useBackward true -set_option backward.isDefEq.respectTransparency.types false @[expose] public section @@ -109,7 +107,6 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] namespace Equivalence -set_option backward.isDefEq.respectTransparency false in @[to_dual existing functor_unitIso_comp] theorem counitIso_functor_comp (e : C ≌ D) (X : C) : dsimp% e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = @@ -117,7 +114,6 @@ theorem counitIso_functor_comp (e : C ≌ D) (X : C) : simpa [functor_unitIso_comp] using Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _) -set_option backward.isDefEq.respectTransparency false in /-- `Equivalence.mk'` is the dual of `Equivalence.mk`, which we need for `to_dual`. Please avoid using this directly. -/ @[to_dual existing mk'] @@ -265,7 +261,6 @@ theorem functor_unit_comp (e : C ≌ D) (X : C) : dsimp% e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) := e.functor_unitIso_comp X -set_option backward.isDefEq.respectTransparency false in @[to_dual counitInv_app_functor] theorem counit_app_functor (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) := by @@ -306,7 +301,6 @@ theorem unit_inverse_comp (e : C ≌ D) (Y : D) : rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app] simp -set_option backward.isDefEq.respectTransparency false in @[to_dual unitInv_app_inverse] theorem unit_app_inverse (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by @@ -340,7 +334,6 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G) _ ≅ F ⋙ G := leftUnitor (F ⋙ G) -set_option backward.isDefEq.respectTransparency false in @[reassoc] theorem adjointify_η_ε (X : C) : F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) := by @@ -369,7 +362,7 @@ instance : Inhabited (C ≌ C) := ⟨refl⟩ /-- Equivalence of categories is symmetric. -/ -@[symm, simps] +@[implicit_reducible, symm, simps] def symm (e : C ≌ D) : D ≌ C := ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counitInv_comp⟩ @@ -482,7 +475,6 @@ theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj /- `cancel_counit_left` is not a `simp` lemma because it would be redundant. -/ -set_option backward.isDefEq.respectTransparency false in @[to_dual cancel_counit_left, simp] theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) : f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono] @@ -581,7 +573,7 @@ instance full_inverse (e : C ≌ E) : e.inverse.Full := /-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is an isomorphism, then there is an equivalence of categories whose functor is `G`. -/ -@[simps!] +@[implicit_reducible, simps!] def changeFunctor (e : C ≌ D) {G : C ⥤ D} (iso : e.functor ≅ G) : C ≌ D where functor := G inverse := e.inverse @@ -597,7 +589,7 @@ theorem changeFunctor_trans (e : C ≌ D) {G G' : C ⥤ D} (iso₁ : e.functor /-- If `e : C ≌ D` is an equivalence of categories, and `iso : e.functor ≅ G` is an isomorphism, then there is an equivalence of categories whose inverse is `G`. -/ -@[simps!] +@[implicit_reducible, simps!] def changeInverse (e : C ≌ D) {G : D ⥤ C} (iso : e.inverse ≅ G) : C ≌ D where functor := e.functor inverse := G @@ -637,13 +629,13 @@ end IsEquivalence /-- A quasi-inverse `D ⥤ C` to a functor that `F : C ⥤ D` that is an equivalence, i.e. faithful, full, and essentially surjective. -/ +@[implicit_reducible] noncomputable def inv (F : C ⥤ D) [F.IsEquivalence] : D ⥤ C where obj X := F.objPreimage X map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) map_id X := by apply F.map_injective; simp map_comp {X Y Z} f g := by apply F.map_injective; simp -set_option backward.isDefEq.respectTransparency false in /-- Interpret a functor that is an equivalence as an equivalence. -/ @[simps functor, simps -isSimp inverse, simps! -isSimp unitIso_hom_app unitIso_inv_app counitIso_hom_app counitIso_inv_app, stacks 02C3] @@ -676,16 +668,15 @@ end Functor namespace Functor - @[simp] theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) : - F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y := by - simpa using! (NatIso.naturality_2 (α := F.asEquivalence.counitIso) (f := f)).symm + F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y := + (NatIso.naturality_2 (α := F.asEquivalence.counitIso) (f := f)).symm @[simp] theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) : - F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y := by - simpa using! (NatIso.naturality_1 (α := F.asEquivalence.unitIso) (f := f)).symm + F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y := + (NatIso.naturality_1 (α := F.asEquivalence.unitIso) (f := f)).symm lemma isEquivalence_of_iso {F G : C ⥤ D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence := ((asEquivalence F).changeFunctor e).isEquivalence_functor diff --git a/Mathlib/CategoryTheory/EssentialImage.lean b/Mathlib/CategoryTheory/EssentialImage.lean index 03c782c1703..f00e504e9e7 100644 --- a/Mathlib/CategoryTheory/EssentialImage.lean +++ b/Mathlib/CategoryTheory/EssentialImage.lean @@ -89,7 +89,7 @@ lemma essImage_ext (F : C ⥤ D) {X Y : F.EssImageSubcategory} (f g : X ⟶ Y) Given a functor `F : C ⥤ D`, we have an (essentially surjective) functor from `C` to the essential image of `F`. -/ -@[simps!] +@[implicit_reducible, simps!] def toEssImage (F : C ⥤ D) : C ⥤ F.EssImageSubcategory := F.essImage.lift F (obj_mem_essImage _) @@ -173,11 +173,10 @@ section variable {J C D : Type*} [Category* J] [Category* C] [Category* D] (G : J ⥤ D) (F : C ⥤ D) [F.Full] [F.Faithful] (hG : ∀ j, F.essImage (G.obj j)) -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Lift a functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` to a functor `G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorCompIso`. -/ -@[simps] def essImage.liftFunctor : J ⥤ C where +@[implicit_reducible, simps] +def essImage.liftFunctor : J ⥤ C where obj j := F.toEssImage.objPreimage ⟨G.obj j, hG j⟩ map {i j} f := F.preimage <| @@ -186,7 +185,6 @@ functor `G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorComp map_id _ := F.map_injective (by simp) map_comp _ _ := F.map_injective (by simp) -set_option backward.isDefEq.respectTransparency false in /-- A functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` does factor through `essImage.liftFunctor G F hG`. -/ @[simps!] def essImage.liftFunctorCompIso : essImage.liftFunctor G F hG ⋙ F ≅ G := diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean index d060ac1d7ed..82a4d0afbdc 100644 --- a/Mathlib/CategoryTheory/Functor/Category.lean +++ b/Mathlib/CategoryTheory/Functor/Category.lean @@ -127,12 +127,10 @@ to_dual_insert_cast hcomp := by ext x; exact β.naturality' (α.app x) /-- Notation for horizontal composition of natural transformations. -/ infixl:80 " ◫ " => hcomp -set_option backward.defeqAttrib.useBackward true in @[to_dual self] theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by simp -set_option backward.defeqAttrib.useBackward true in @[to_dual self] theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by simp diff --git a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean index d7b7098026f..df388bbf593 100644 --- a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean +++ b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean @@ -217,7 +217,6 @@ def isoEquiv {X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y) where left_inv := by cat_disch right_inv := by cat_disch -set_option backward.isDefEq.respectTransparency false in /-- Fully faithful functors are stable by composition. -/ @[simps] def comp {G : D ⥤ E} (hG : G.FullyFaithful) : (F ⋙ G).FullyFaithful where @@ -351,7 +350,6 @@ theorem Faithful.div_faithful (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithf Functor.Faithful (Faithful.div F G obj @h_obj @map @h_map) := (Faithful.div_comp F G _ h_obj _ @h_map).faithful_of_comp -set_option backward.isDefEq.respectTransparency false in instance Full.comp [Full F] [Full G] : Full (F ⋙ G) where map_surjective f := ⟨F.preimage (G.preimage f), by simp⟩ @@ -365,7 +363,6 @@ lemma Full.of_comp_faithful_iso {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [Full have := Full.of_iso h.symm exact Full.of_comp_faithful F G -set_option backward.isDefEq.respectTransparency false in /-- Given a natural isomorphism between `F ⋙ H` and `G ⋙ H` for a fully faithful functor `H`, we can 'cancel' it to give a natural iso between `F` and `G`. -/ diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean index 209218a4748..4b3d2d4e4ad 100644 --- a/Mathlib/CategoryTheory/Limits/Cones.lean +++ b/Mathlib/CategoryTheory/Limits/Cones.lean @@ -32,8 +32,6 @@ And, of course, we dualise all this to cocones as well. For more results about the category of cones, see `cone_category.lean`. -/ -set_option backward.defeqAttrib.useBackward true - @[expose] public section -- morphism levels before object levels. See note [category theory universes]. @@ -65,7 +63,7 @@ variable (F : J ⥤ C) type of natural transformations from the constant functor with value `X` to `F`. An object representing this functor is a limit of `F`. -/ -@[simps! obj map] +@[implicit_reducible, simps! obj map] def cones : Cᵒᵖ ⥤ Type (max u₁ v₃) := (const J).op ⋙ yoneda.obj F @@ -73,7 +71,7 @@ def cones : Cᵒᵖ ⥤ Type (max u₁ v₃) := the type of natural transformations from `F` to the constant functor with value `X`. An object corepresenting this functor is a colimit of `F`. -/ -@[simps! obj map] +@[implicit_reducible, simps! obj map] def cocones : C ⥤ Type (max u₁ v₃) := const J ⋙ coyoneda.obj (op F) @@ -150,8 +148,6 @@ instance inhabitedCone (F : Discrete PUnit ⥤ C) : Inhabited (Cone F) := } }⟩ -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in @[to_dual (attr := reassoc), elementwise] theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') : dsimp% c.π.app j ≫ F.map f = c.π.app j' := by @@ -201,14 +197,14 @@ def extensions (c : Cone F) : uliftYoneda.obj c.pt ⟶ F.cones where app _ := ↾fun f ↦ (const J).map f.down ≫ c.π /-- A map to the vertex of a cone induces a cone by composition. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- A map from the vertex of a cocone induces a cocone by composition. -/] def extend (c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F where pt := X π := (const J).map f ≫ c.π /-- Whisker a cone by precomposition of a functor. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Whisker a cocone by precomposition of a functor. See `whiskering` for a functorial version. -/] @@ -262,12 +258,10 @@ structure CoconeMorphism (A B : Cocone F) where attribute [reassoc (attr := simp)] ConeMorphism.w CoconeMorphism.w attribute [to_dual existing] ConeMorphism.casesOn -set_option backward.isDefEq.respectTransparency.types false in @[to_dual] instance inhabitedConeMorphism (A : Cone F) : Inhabited (ConeMorphism A A) := ⟨{ hom := 𝟙 _ }⟩ -set_option backward.isDefEq.respectTransparency.types false in /-- The category of cones on a given diagram. -/ @[to_dual (attr := simps) /-- The category of cocones on a given diagram. -/] instance Cone.category : Category (Cone F) where @@ -275,7 +269,6 @@ instance Cone.category : Category (Cone F) where comp f g := { hom := f.hom ≫ g.hom } id B := { hom := 𝟙 B.pt } -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := ext) /- We do not want `simps` automatically generate the lemma for simplifying the hom field of a category. So we need to write the `ext` lemma in terms of the @@ -285,25 +278,20 @@ theorem ConeMorphism.ext {c c' : Cone F} (f g : c ⟶ c') (w : f.hom = g.hom) : cases g congr -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp))] lemma ConeMorphism.hom_inv_id {c d : Cone F} (f : c ≅ d) : f.hom.hom ≫ f.inv.hom = 𝟙 _ := by simp [← Cone.category_comp_hom] -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp))] lemma ConeMorphism.inv_hom_id {c d : Cone F} (f : c ≅ d) : f.inv.hom ≫ f.hom.hom = 𝟙 _ := by simp [← Cone.category_comp_hom] -set_option backward.isDefEq.respectTransparency.types false in @[to_dual] instance {c d : Cone F} (f : c ≅ d) : IsIso f.hom.hom := ⟨f.inv.hom, by simp⟩ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual] instance {c d : Cone F} (f : c ≅ d) : IsIso f.inv.hom := ⟨f.hom.hom, by simp⟩ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp))] lemma ConeMorphism.map_w {c c' : Cone F} (f : c ⟶ c') (G : C ⥤ D) (j : J) : G.map f.hom ≫ G.map (c'.π.app j) = G.map (c.π.app j) := by @@ -311,7 +299,6 @@ lemma ConeMorphism.map_w {c c' : Cone F} (f : c ⟶ c') (G : C ⥤ D) (j : J) : namespace Cone -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps. -/ @@ -328,7 +315,6 @@ def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt) attribute [to_dual existing extInv_inv_hom] ext_hom_hom attribute [to_dual existing extInv_hom_hom] ext_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps. -/ @@ -344,7 +330,6 @@ attribute [to_dual existing ext_inv_hom] extInv_hom_hom attribute [aesop apply safe (rule_sets := [CategoryTheory])] Limits.Cone.ext Limits.Cocone.ext -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- Eta rule for cones. -/ @[to_dual (attr := simps!) /-- Eta rule for cocones. -/] @@ -365,13 +350,11 @@ theorem cone_iso_of_hom_iso {K : J ⥤ C} {c d : Cone K} (f : c ⟶ d) [i : IsIs ⟨⟨{ hom := inv f.hom w := fun j => (asIso f.hom).inv_comp_eq.2 (f.w j).symm }, by cat_disch⟩⟩ -set_option backward.isDefEq.respectTransparency.types false in /-- There is a morphism from an extended cone to the original cone. -/ @[to_dual (attr := simps) /-- There is a morphism from a cocone to its extension. -/] def extendHom (s : Cone F) {X : C} (f : X ⟶ s.pt) : s.extend f ⟶ s where hom := f -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- Extending a cone by the identity does nothing. -/ @[to_dual (attr := simps!) /-- Extending a cocone by the identity does nothing. -/] @@ -381,7 +364,6 @@ def extendId (s : Cone F) : s.extend (𝟙 s.pt) ≅ s := attribute [to_dual existing extendId_inv_hom] extendId_hom_hom attribute [to_dual existing extendId_hom_hom] extendId_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- Extending a cone by a composition is the same as extending the cone twice. -/ @[to_dual (attr := simps!) (reorder := f g) @@ -393,7 +375,6 @@ def extendComp (s : Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : attribute [to_dual existing extendComp_inv_hom] extendComp_hom_hom attribute [to_dual existing extendComp_hom_hom] extendComp_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- A cone extended by an isomorphism is isomorphic to the original cone. -/ @[to_dual (attr := simps) @@ -409,11 +390,10 @@ attribute [to_dual existing extendIso_hom_hom] extendIso_inv_hom instance {s : Cone F} {X : C} (f : X ⟶ s.pt) [IsIso f] : IsIso (s.extendHom f) := ⟨(extendIso s (asIso' f)).hom, by cat_disch⟩ -set_option backward.isDefEq.respectTransparency.types false in /-- Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone for `G`. -/] def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G where @@ -422,7 +402,6 @@ def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G where π := c.π ≫ α } map f := { hom := f.hom } -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as postcomposing by `α` and then by `β`. -/ @@ -436,7 +415,6 @@ def postcomposeComp {G H : J ⥤ C} (α : F ⟶ G) (β : G ⟶ H) : attribute [to_dual existing precomposeComp_inv_app_hom] postcomposeComp_hom_app_hom attribute [to_dual existing precomposeComp_hom_app_hom] postcomposeComp_inv_app_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- Postcomposing by the identity does not change the cone up to isomorphism. -/ @[to_dual (attr := simps!) @@ -447,11 +425,10 @@ def postcomposeId : postcompose (𝟙 F) ≅ 𝟭 (Cone F) := attribute [to_dual existing precomposeId_inv_app_hom] postcomposeId_hom_app_hom attribute [to_dual existing precomposeId_hom_app_hom] postcomposeId_inv_app_hom -set_option backward.isDefEq.respectTransparency.types false in /-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of cones. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of cocones. -/] @@ -463,14 +440,13 @@ def postcomposeEquivalence {G : J ⥤ C} (α : F ≅ G) : Cone F ≌ Cone G wher /-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cone F` to `Cone (E ⋙ F)`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cocone F` to `Cocone (E ⋙ F)`. -/] def whiskering (E : K ⥤ J) : Cone F ⥤ Cone (E ⋙ F) where obj c := c.whisker E map f := { hom := f.hom } -set_option backward.isDefEq.respectTransparency.types false in /-- Whiskering by an equivalence gives an equivalence between categories of cones. -/ @[to_dual (attr := simps) @@ -510,9 +486,8 @@ def forget : Cone F ⥤ C where variable (G : C ⥤ D) -set_option backward.isDefEq.respectTransparency.types false in /-- A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially. -/] def functoriality : Cone F ⥤ Cone (F ⋙ G) where obj A := @@ -524,14 +499,12 @@ def functoriality : Cone F ⥤ Cone (F ⋙ G) where { hom := G.map f.hom w := ConeMorphism.map_w f G } -set_option backward.isDefEq.respectTransparency.types false in /-- Functoriality is functorial. -/ @[to_dual /-- Functoriality is functorial. -/] def functorialityCompFunctoriality (H : D ⥤ E) : functoriality F G ⋙ functoriality (F ⋙ G) H ≅ functoriality F (G ⋙ H) := NatIso.ofComponents (fun _ ↦ Iso.refl _) -set_option backward.isDefEq.respectTransparency.types false in @[to_dual] instance functoriality_full [G.Full] [G.Faithful] : (functoriality F G).Full where map_surjective t := @@ -597,7 +570,6 @@ namespace Cones @[deprecated (since := "2026-03-06")] alias equivalenceOfReindexing := Cone.equivalenceOfReindexing @[deprecated (since := "2026-03-06")] alias forget := Cone.forget @[deprecated (since := "2026-03-06")] alias functoriality := Cone.functoriality -set_option backward.isDefEq.respectTransparency.types false in @[deprecated (since := "2026-03-06")] alias functorialityCompFunctoriality := Cone.functorialityCompFunctoriality @[deprecated (since := "2026-03-06")] alias functoriality_full := Cone.functoriality_full @@ -628,7 +600,6 @@ namespace Cocones alias equivalenceOfReindexing := Cocone.equivalenceOfReindexing @[deprecated (since := "2026-03-06")] alias forget := Cocone.forget @[deprecated (since := "2026-03-06")] alias functoriality := Cocone.functoriality -set_option backward.isDefEq.respectTransparency.types false in @[deprecated (since := "2026-03-06")] alias functorialityCompFunctoriality := Cocone.functorialityCompFunctoriality @[deprecated (since := "2026-03-06")] alias functoriality_full := Cocone.functoriality_full @@ -649,12 +620,11 @@ variable (H : C ⥤ D) {F : J ⥤ C} {G : J ⥤ C} open CategoryTheory.Limits /-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/ -@[to_dual (attr := simps!) +@[to_dual (attr := implicit_reducible, simps!) /-- The image of a cocone in C under a functor G : C ⥤ D is a cocone in D. -/] def mapCone (c : Cone F) : Cone (F ⋙ H) := (Cone.functoriality F H).obj c -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- The construction `mapCone` respects functor composition. -/ @[to_dual (attr := simps!) @@ -693,7 +663,6 @@ noncomputable def mapConeInvMapCone {F : J ⥤ D} (H : D ⥤ C) [IsEquivalence H mapConeInv H (mapCone H c) ≅ c := (Limits.Cone.functorialityEquivalence F (asEquivalence H)).unitIso.symm.app c -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- `functoriality F _ ⋙ postcompose (whisker_left F _)` simplifies to `functoriality F _`. -/ @[to_dual (attr := simps!) @@ -707,7 +676,6 @@ attribute [to_dual existing functorialityCompPrecompose_inv_app_hom] attribute [to_dual existing functorialityCompPrecompose_hom_app_hom] functorialityCompPostcompose_inv_app_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- For `F : J ⥤ C`, given a cone `c : Cone F`, and a natural isomorphism `α : H ≅ H'` for functors `H H' : C ⥤ D`, the postcomposition of the cone `H.mapCone` using the isomorphism `α` is @@ -728,7 +696,6 @@ attribute [to_dual existing precomposeWhiskerLeftMapCocone_inv_hom] attribute [to_dual existing precomposeWhiskerLeftMapCocone_hom_hom] postcomposeWhiskerLeftMapCone_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- `mapCone` commutes with `postcompose`. In particular, for `F : J ⥤ C`, given a cone `c : Cone F`, a @@ -748,7 +715,6 @@ def mapConePostcompose {α : F ⟶ G} {c} : attribute [to_dual existing mapCoconePrecompose_inv_hom] mapConePostcompose_hom_hom attribute [to_dual existing mapCoconePrecompose_hom_hom] mapConePostcompose_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- `mapCone` commutes with `postcomposeEquivalence` -/ @[to_dual (attr := simps!) /-- `mapCocone` commutes with `precomposeEquivalence` -/] @@ -762,7 +728,6 @@ attribute [to_dual existing mapCoconePrecomposeEquivalenceFunctor_inv_hom] attribute [to_dual existing mapCoconePrecomposeEquivalenceFunctor_hom_hom] mapConePostcomposeEquivalenceFunctor_inv_hom -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- `mapCone` commutes with `whisker` -/ @[to_dual (attr := simps!) /-- `mapCocone` commutes with `whisker` -/] @@ -781,20 +746,19 @@ section variable {F : J ⥤ C} /-- Change a `Cone F` into a `Cocone F.op`. -/ -@[to_dual (attr := simps) /-- Change a `Cocone F` into a `Cone F.op`. -/] +@[to_dual (attr := implicit_reducible, simps) /-- Change a `Cocone F` into a `Cone F.op`. -/] def Cone.op (c : Cone F) : Cocone F.op where pt := Opposite.op c.pt ι := NatTrans.op c.π /-- Change a `Cone F.op` into a `Cocone F`. -/ -@[to_dual (attr := simps) /-- Change a `Cocone F.op` into a `Cone F`. -/] +@[to_dual (attr := implicit_reducible, simps) /-- Change a `Cocone F.op` into a `Cone F`. -/] def Cone.unop (c : Cone F.op) : Cocone F where pt := Opposite.unop c.pt ι := NatTrans.removeOp c.π variable (F) -set_option backward.isDefEq.respectTransparency false in /-- The category of cocones on `F` is equivalent to the opposite category of the category of cones on the opposite of `F`. -/ @@ -823,7 +787,6 @@ def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ where unitIso := Iso.refl _ counitIso := Iso.refl _ -set_option backward.isDefEq.respectTransparency.types false in /-- Cones on `F : J ⥤ C` are equivalent to cocones on `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/ @[to_dual (attr := simps) /-- Cocones on `F : J ⥤ C` are equivalent to cones on `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/] @@ -842,20 +805,19 @@ section variable {F : J ⥤ Cᵒᵖ} /-- Change a cocone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/ -@[to_dual (attr := simps!) +@[to_dual (attr := implicit_reducible, simps!) /-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/] def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F where pt := op c.pt π := NatTrans.removeLeftOp c.ι /-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.leftOp : Jᵒᵖ ⥤ C`. -/ -@[to_dual (attr := simps!) +@[to_dual (attr := implicit_reducible, simps!) /-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.leftOp : Jᵒᵖ ⥤ C`. -/] def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp where pt := unop c.pt ι := NatTrans.leftOp c.π -set_option backward.isDefEq.respectTransparency.types false in /-- Cones on `F : J ⥤ Cᵒᵖ` are equivalent to cocones on `F.leftOp : Jᵒᵖ ⥤ C`. -/ @[to_dual (attr := simps) /-- Cocones on `F : J ⥤ Cᵒᵖ` are equivalent to cones on `F.leftOp : Jᵒᵖ ⥤ C`. -/] @@ -874,20 +836,19 @@ section variable {F : Jᵒᵖ ⥤ C} /-- Change a cocone on `F.rightOp : J ⥤ Cᵒᵖ` to a cone on `F : Jᵒᵖ ⥤ C`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Change a cone on `F.rightOp : J ⥤ Cᵒᵖ` to a cocone on `F : Jᵒᵖ ⥤ C`. -/] def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F where pt := unop c.pt π := NatTrans.removeRightOp c.ι /-- Change a cone on `F : Jᵒᵖ ⥤ C` to a cocone on `F.rightOp : Jᵒᵖ ⥤ C`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Change a cocone on `F : Jᵒᵖ ⥤ C` to a cone on `F.rightOp : J ⥤ Cᵒᵖ`. -/] def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp where pt := op c.pt ι := NatTrans.rightOp c.π -set_option backward.isDefEq.respectTransparency.types false in /-- Cones on `F : Jᵒᵖ ⥤ C` are equivalent to cocones on `F.rightOp : J ⥤ Cᵒᵖ`. -/ @[to_dual (attr := simps) /-- Cocones on `F : Jᵒᵖ ⥤ C` are equivalent to cones on `F.rightOp : J ⥤ Cᵒᵖ`. -/] @@ -906,20 +867,19 @@ section variable {F : Jᵒᵖ ⥤ Cᵒᵖ} /-- Change a cocone on `F.unop : J ⥤ C` into a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Change a cone on `F.unop : J ⥤ C` into a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/] def coneOfCoconeUnop (c : Cocone F.unop) : Cone F where pt := op c.pt π := NatTrans.removeUnop c.ι /-- Change a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cocone on `F.unop : J ⥤ C`. -/ -@[to_dual (attr := simps) +@[to_dual (attr := implicit_reducible, simps) /-- Change a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cone on `F.unop : J ⥤ C`. -/] def coconeUnopOfCone (c : Cone F) : Cocone F.unop where pt := unop c.pt ι := NatTrans.unop c.π -set_option backward.isDefEq.respectTransparency.types false in /-- Cones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cocones on `F.unop : J ⥤ C`. -/ @[to_dual (attr := simps) /-- Cocones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cones on `F.unop : J ⥤ C`. -/] @@ -941,7 +901,6 @@ open CategoryTheory.Limits variable {F : J ⥤ C} (G : C ⥤ D) -set_option backward.isDefEq.respectTransparency.types false in set_option linter.translate.warnInvalid false in /-- The opposite cocone of the image of a cone is the image of the opposite cocone. -/ @[to_dual (attr := simps!) diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean index b92a031ebd3..de2746e77dc 100644 --- a/Mathlib/CategoryTheory/Limits/HasLimits.lean +++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean @@ -228,7 +228,6 @@ theorem limit.existsUnique {F : J ⥤ C} [HasLimit F] (t : Cone F) : def limit.isoLimitCone {F : J ⥤ C} [HasLimit F] (t : LimitCone F) : limit F ≅ t.cone.pt := IsLimit.conePointUniqueUpToIso (limit.isLimit F) t.isLimit -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem limit.isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) : (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j := by @@ -250,7 +249,6 @@ instance isIso_limMap {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [ IsIso (limMap α) := ⟨limMap (inv α), by cat_disch , by cat_disch⟩ -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem limit.lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) : limit.lift F c ≫ limMap α = limit.lift G ((Cone.postcompose α).obj c) := by @@ -284,7 +282,6 @@ def limit.homIso' (F : J ⥤ C) [HasLimit F] (W : C) : { p : ∀ j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' } := (limit.isLimit F).homIso' W -set_option backward.isDefEq.respectTransparency false in theorem limit.lift_extend {F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) : limit.lift F (c.extend f) = f ≫ limit.lift F c := by cat_disch @@ -344,7 +341,6 @@ def HasLimit.isoOfEquivalence {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit IsLimit.conePointsIsoOfEquivalence (limit.isLimit F) (limit.isLimit G) e w set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem HasLimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) : @@ -354,7 +350,6 @@ theorem HasLimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C simp set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem HasLimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) : @@ -373,12 +368,10 @@ variable [HasLimit F] (E : K ⥤ J) [HasLimit (E ⋙ F)] def limit.pre : limit F ⟶ limit (E ⋙ F) := limit.lift (E ⋙ F) ((limit.cone F).whisker E) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) := by simp [limit.pre] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem limit.lift_pre (c : Cone F) : limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) := by ext; simp @@ -394,7 +387,6 @@ theorem limit.pre_pre [h : HasLimit (D ⋙ E ⋙ F)] : haveI : HasLimit ((D ⋙ variable {E F} -set_option backward.isDefEq.respectTransparency false in /-- If we have particular limit cones available for `E ⋙ F` and for `F`, we obtain a formula for `limit.pre F E`. @@ -415,12 +407,10 @@ variable (F : J ⥤ C) [HasLimit F] (G : C ⥤ D) [HasLimit (F ⋙ G)] def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) := limit.lift (F ⋙ G) (G.mapCone (limit.cone F)) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) := by simp [limit.post] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem limit.lift_post (c : Cone F) : G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c) := by @@ -488,7 +478,6 @@ def lim : (J ⥤ C) ⥤ C where apply Limits.limit.hom_ext; intro j simp [assoc] -set_option backward.isDefEq.respectTransparency false in /-- The natural transformation induced by `limit.π`. -/ @[simps] def lim.π (j : J) : lim ⟶ (evaluation J C).obj j where @@ -500,13 +489,11 @@ variable {G : J ⥤ C} (α : F ⟶ G) theorem limMap_eq : limMap α = lim.map α := rfl -set_option backward.isDefEq.respectTransparency false in theorem limit.map_pre [HasLimitsOfShape K C] (E : K ⥤ J) : lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α) := by ext simp -set_option backward.isDefEq.respectTransparency false in theorem limit.map_pre' [HasLimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) : limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whiskerRight α F) := by ext1; simp @@ -532,8 +519,6 @@ def limYoneda : lim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cones J C := NatIso.ofComponents fun F => NatIso.ofComponents fun W => limit.homIso F (unop W) -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The constant functor and limit functor are adjoint to each other -/ def constLimAdj : (const J : C ⥤ J ⥤ C) ⊣ lim := Adjunction.mk' { homEquiv := fun c g ↦ @@ -811,7 +796,6 @@ theorem colimit.isoColimitCocone_ι_hom {F : J ⥤ C} [HasColimit F] (t : Colimi dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso] simp -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem colimit.isoColimitCocone_ι_inv {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) : t.cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j := by @@ -855,7 +839,6 @@ def colimit.homIso' (F : J ⥤ C) [HasColimit F] (W : C) : { p : ∀ j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j } := (colimit.isColimit F).homIso' W -set_option backward.isDefEq.respectTransparency false in theorem colimit.desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) : colimit.desc F (c.extend f) = colimit.desc F c ≫ f := by ext; simp @@ -916,7 +899,6 @@ def HasColimit.isoOfEquivalence {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasC IsColimit.coconePointsIsoOfEquivalence (colimit.isColimit F) (colimit.isColimit G) e w set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem HasColimit.ι_isoOfEquivalence_hom {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) : @@ -925,7 +907,6 @@ theorem HasColimit.ι_isoOfEquivalence_hom {F : J ⥤ C} [HasColimit F] {G : K simp [HasColimit.isoOfEquivalence] set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem HasColimit.ι_isoOfEquivalence_inv {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) : @@ -949,7 +930,6 @@ variable [HasColimit F] (E : K ⥤ J) [HasColimit (E ⋙ F)] def colimit.pre : colimit (E ⋙ F) ⟶ colimit F := colimit.desc (E ⋙ F) ((colimit.cocone F).whisker E) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) := by simp [colimit.pre] @@ -959,7 +939,6 @@ theorem colimit.ι_inv_pre [IsIso (pre F E)] (k : K) : colimit.ι F (E.obj k) ≫ inv (colimit.pre F E) = colimit.ι (E ⋙ F) k := by simp [IsIso.comp_inv_eq] -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem colimit.pre_desc (c : Cocone F) : colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) := by @@ -980,7 +959,6 @@ theorem colimit.pre_pre [h : HasColimit (D ⋙ E ⋙ F)] : variable {E F} -set_option backward.isDefEq.respectTransparency false in /-- If we have particular colimit cocones available for `E ⋙ F` and for `F`, we obtain a formula for `colimit.pre F E`. @@ -1005,13 +983,11 @@ to `G` applied to the colimit of `F`. def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) := colimit.desc (F ⋙ G) (G.mapCocone (colimit.cocone F)) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) := by simp [colimit.post] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem colimit.post_desc (c : Cocone F) : colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c) := by @@ -1076,7 +1052,6 @@ def colim : (J ⥤ C) ⥤ C where obj F := colimit F map α := colimMap α -set_option backward.isDefEq.respectTransparency false in /-- The natural transformation induced by `colimit.ι`. -/ @[simps] def colim.ι (j : J) : (evaluation J C).obj j ⟶ colim where @@ -1088,35 +1063,29 @@ variable {G : J ⥤ C} (α : F ⟶ G) theorem colimMap_eq : colimMap α = colim.map α := rfl -set_option backward.isDefEq.respectTransparency false in -- This seems to be needed in downstream files. @[reassoc] theorem colimit.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j := by simp -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem colimit.map_desc (c : Cocone G) : colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocone.precompose α).obj c) := by ext j simp [colimit.ι_desc, colimit.ι_desc] -set_option backward.isDefEq.respectTransparency false in theorem colimit.pre_map [HasColimitsOfShape K C] (E : K ⥤ J) : colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E := by ext rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre] rfl -set_option backward.isDefEq.respectTransparency false in theorem colimit.pre_map' [HasColimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) : colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂ := by ext1 simp -set_option backward.defeqAttrib.useBackward true in theorem colimit.pre_id (F : J ⥤ C) : colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom := by cat_disch -set_option backward.isDefEq.respectTransparency false in theorem colimit.map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D] (H : C ⥤ D) : /- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs @@ -1139,8 +1108,6 @@ def colimCoyoneda : colim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftF ≅ CategoryTheory.cocones J C := NatIso.ofComponents fun F => NatIso.ofComponents fun W => colimit.homIso (unop F) W -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The colimit functor and constant functor are adjoint to each other -/ def colimConstAdj : (colim : (J ⥤ C) ⥤ C) ⊣ const J := Adjunction.mk' { @@ -1212,7 +1179,6 @@ end Colimit section Opposite -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- If `t : Cone F` is a limit cone, then `t.op : Cocone F.op` is a colimit cocone. -/ @@ -1228,7 +1194,6 @@ def IsLimit.op {t : Cone F} (P : IsLimit t) : IsColimit t.op where rw [← w] rfl -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- If `t : Cocone F` is a colimit cocone, then `t.op : Cone F.op` is a limit cone. -/ diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean index 76d8b75138b..74de4a1b949 100644 --- a/Mathlib/CategoryTheory/Limits/IsLimit.lean +++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean @@ -61,7 +61,6 @@ structure IsLimit (t : Cone F) where uniq : ∀ (s : Cone F) (m : s.pt ⟶ t.pt) (_ : ∀ j : J, m ≫ t.π.app j = s.π.app j), m = lift s := by cat_disch -set_option backward.defeqAttrib.useBackward true in /-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique cocone morphism from `t`. -/ @[stacks 002F, to_dual] @@ -93,9 +92,6 @@ of a colimit cocone over `F` to the cocone point of any cocone over `G`. -/] def map {F G : J ⥤ C} (s : Cone F) {t : Cone G} (P : IsLimit t) (α : F ⟶ G) : s.pt ⟶ t.pt := P.lift ((Cone.postcompose α).obj s) -#adaptation_note -/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp)) (reorder := c hd d) ι_map] theorem map_π {F G : J ⥤ C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) : hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j := @@ -178,13 +174,11 @@ theorem conePointUniqueUpToIso_inv_comp {s t : Cone F} (P : IsLimit s) (Q : IsLi (conePointUniqueUpToIso P Q).inv ≫ s.π.app j = t.π.app j := (uniqueUpToIso P Q).inv.w _ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_inv_desc] theorem lift_comp_conePointUniqueUpToIso_hom {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : P.lift r ≫ (conePointUniqueUpToIso P Q).hom = Q.lift r := Q.uniq _ _ (by simp) -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp)) coconePointUniqueUpToIso_hom_desc] theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r := @@ -236,14 +230,11 @@ def ofPointIso {r t : Cone F} (P : IsLimit r) [i : IsIso (P.lift t)] : IsLimit t variable {t : Cone F} -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in @[to_dual] theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.pt) : m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } } := h.uniq { pt := W, π := { app := fun b => m ≫ t.π.app b } } m fun _ => rfl -set_option backward.isDefEq.respectTransparency.types false in /-- Two morphisms into a limit are equal if their compositions with each cone morphism are equal. -/ @[to_dual /-- Two morphisms out of a colimit are equal if their compositions with @@ -253,7 +244,6 @@ theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.pt} f = f' := by rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w -set_option backward.isDefEq.respectTransparency.types false in @[to_dual] lemma nonempty_isLimit_iff_isIso_lift {s t : Cone F} (hs : IsLimit s) : Nonempty (IsLimit t) ↔ IsIso (hs.lift t) := @@ -347,7 +337,6 @@ def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) (d : Cone G) (w : (Cone.postcompose α.hom).obj c ≅ d) : IsLimit c ≃ IsLimit d := (postcomposeHomEquiv α _).symm.trans (equivIsoLimit w) -set_option backward.defeqAttrib.useBackward true in set_option linter.translate.warnInvalid false in /-- The cone points of two limit cones for naturally isomorphic functors are themselves isomorphic. @@ -368,7 +357,6 @@ attribute [to_dual existing coconePointsIsoOfNatIso_hom] conePointsIsoOfNatIso_i #adaptation_note /-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc) comp_coconePointsIsoOfNatIso_inv] theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) : @@ -376,7 +364,6 @@ theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} #adaptation_note /-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc) comp_coconePointsIsoOfNatIso_hom] theorem conePointsIsoOfNatIso_inv_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) : @@ -445,7 +432,6 @@ def extendIsoEquiv {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] : equivOfSubsingletonOfSubsingleton (extendIso i) (ofExtendIso i) set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in set_option linter.translate.warnInvalid false in /-- We can prove two cone points `(s : Cone F).pt` and `(t : Cone G).pt` are isomorphic if * both cones are limit cones @@ -487,7 +473,6 @@ attribute [to_dual existing coconePointsIsoOfEquivalence_hom] conePointsIsoOfEqu end Equivalence -set_option backward.defeqAttrib.useBackward true in /-- The universal property of a limit cone: a map `W ⟶ t.pt` is the same as a cone on `F` with cone point `W`. -/ @[to_dual (attr := simps apply) @@ -499,14 +484,12 @@ def homEquiv (h : IsLimit t) {W : C} : (W ⟶ t.pt) ≃ ((Functor.const J).obj W left_inv f := h.hom_ext (by simp) right_inv π := by cat_disch -set_option backward.isDefEq.respectTransparency.types false in @[to_dual (attr := reassoc (attr := simp)) ι_app_homEquiv_symm] lemma homEquiv_symm_π_app (h : IsLimit t) {W : C} (f : (const J).obj W ⟶ F) (j : J) : h.homEquiv.symm f ≫ t.π.app j = f.app j := by simp [homEquiv] -set_option backward.defeqAttrib.useBackward true in @[to_dual] lemma homEquiv_symm_naturality (h : IsLimit t) {W W' : C} (f : (const J).obj W ⟶ F) (g : W' ⟶ W) : @@ -533,7 +516,6 @@ set_option backward.defeqAttrib.useBackward true in def natIso (h : IsLimit t) : yoneda.obj t.pt ⋙ uliftFunctor.{u₁} ≅ F.cones := by refine NatIso.ofComponents (fun W => IsLimit.homIso h (unop W)) -set_option backward.defeqAttrib.useBackward true in /-- Another, more explicit, formulation of the universal property of a limit cone. See also `homIso`. -/ def homIso' (h : IsLimit t) (W : C) : @@ -594,6 +576,7 @@ variable {X : C} (h : F.cones.RepresentableBy X) /-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point `Y`. -/ +@[implicit_reducible] def coneOfHom {Y : C} (f : Y ⟶ X) : Cone F where pt := Y π := h.homEquiv f @@ -610,13 +593,13 @@ theorem coneOfHom_homOfCone (s : Cone F) : coneOfHom h (homOfCone h s) = s := by congr exact h.homEquiv.apply_symm_apply s_π -set_option backward.isDefEq.respectTransparency false in @[simp] theorem homOfCone_coneOfHom {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f := by simp [coneOfHom, homOfCone] /-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X` will be a limit cone. -/ +@[implicit_reducible] def limitCone : Cone F := coneOfHom h (𝟙 X) @@ -641,7 +624,6 @@ section open OfNatIso -set_option backward.isDefEq.respectTransparency.types false in /-- If `F.cones` is representable, then the cone corresponding to the identity morphism on the representing object is a limit cone. -/ @@ -689,7 +671,6 @@ set_option backward.defeqAttrib.useBackward true in def natIso (h : IsColimit t) : coyoneda.obj (op t.pt) ⋙ uliftFunctor.{u₁} ≅ F.cocones := NatIso.ofComponents (IsColimit.homIso h) -set_option backward.defeqAttrib.useBackward true in /-- Another, more explicit, formulation of the universal property of a colimit cocone. See also `homIso`. -/ def homIso' (h : IsColimit t) (W : C) : @@ -703,7 +684,6 @@ def homIso' (h : IsColimit t) (W : C) : naturality := fun j j' f => by dsimp; rw [comp_id]; exact p.2 f } } -set_option backward.defeqAttrib.useBackward true in /-- A cocone is a colimit cocone exactly if there is a unique cocone morphism from any other cocone. -/ @@ -722,6 +702,7 @@ variable {X : C} (h : F.cocones.CorepresentableBy X) /-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone point `Y`. -/ +@[implicit_reducible] def coconeOfHom {Y : C} (f : X ⟶ Y) : Cocone F where pt := Y ι := h.homEquiv f @@ -738,13 +719,13 @@ theorem coconeOfHom_homOfCocone (s : Cocone F) : coconeOfHom h (homOfCocone h s) congr exact h.homEquiv.apply_symm_apply s_ι -set_option backward.isDefEq.respectTransparency false in @[simp] theorem homOfCocone_coconeOfHom {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f := by simp [homOfCocone, coconeOfHom] /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X` will be a colimit cocone. -/ +@[implicit_reducible] def colimitCocone : Cocone F := coconeOfHom h (𝟙 X) @@ -769,7 +750,6 @@ section open OfNatIso -set_option backward.isDefEq.respectTransparency.types false in /-- If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on the representing object is a colimit cocone. -/ diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index 350bffea695..0435283dd9e 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -114,8 +114,9 @@ theorem walkingParallelPairHom_id (X : WalkingParallelPair) : WalkingParallelPai /-- The functor `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to right. -/ +@[implicit_reducible] def walkingParallelPairOp : WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ where - obj x := op <| by cases x; exacts [one, zero] + obj x := op <| match x with | zero => one | one => zero map f := by cases f <;> apply Quiver.Hom.op exacts [left, right, WalkingParallelPairHom.id _] @@ -135,8 +136,6 @@ theorem walkingParallelPairOp_left : theorem walkingParallelPairOp_right : walkingParallelPairOp.map right = @Quiver.Hom.op _ _ zero one right := rfl -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- The equivalence `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to right. @@ -253,6 +252,7 @@ variable [Category.{v} C] open parallelPair in /-- `parallelPair f g` is the diagram in `C` consisting of the two morphisms `f` and `g` with common domain and codomain. -/ +@[implicit_reducible] def parallelPair (f g : X ⟶ Y) : WalkingParallelPair ⥤ C where obj x := parallelPairObj X Y x map h := parallelPairHom f g h @@ -274,7 +274,6 @@ theorem parallelPair_map_right (f g : X ⟶ Y) : (parallelPair f g).map right = theorem parallelPair_functor_obj {F : WalkingParallelPair ⥤ C} (j : WalkingParallelPair) : (parallelPair (F.map left) (F.map right)).obj j = F.obj j := by cases j <;> rfl -set_option backward.isDefEq.respectTransparency.types false in /-- Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a `parallelPair` -/ @[simps!] @@ -374,27 +373,22 @@ def Cofork.π (t : Cofork f g) : Y ⟶ t.pt := theorem Cofork.app_one_eq_π (t : Cofork f g) : t.ι.app one = t.π := rfl -set_option backward.isDefEq.respectTransparency false in @[simp] theorem Fork.app_one_eq_ι_comp_left (s : Fork f g) : s.π.app one = s.ι ≫ f := by rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left] -set_option backward.isDefEq.respectTransparency false in @[reassoc] theorem Fork.app_one_eq_ι_comp_right (s : Fork f g) : s.π.app one = s.ι ≫ g := by rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem Cofork.app_zero_eq_comp_π_left (s : Cofork f g) : s.ι.app zero = f ≫ s.π := by rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left] -set_option backward.isDefEq.respectTransparency false in @[reassoc] theorem Cofork.app_zero_eq_comp_π_right (s : Cofork f g) : s.ι.app zero = g ≫ s.π := by rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right] -set_option backward.defeqAttrib.useBackward true in /-- A fork on `f g : X ⟶ Y` is determined by the morphism `ι : P ⟶ X` satisfying `ι ≫ f = ι ≫ g`. -/ @[simps, implicit_reducible] @@ -408,7 +402,6 @@ def Fork.ofι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : Fork f g where naturality := fun {X} {Y} f => by cases X <;> cases Y <;> cases f <;> simp [w] } -set_option backward.defeqAttrib.useBackward true in /-- A cofork on `f g : X ⟶ Y` is determined by the morphism `π : Y ⟶ P` satisfying `f ≫ π = g ≫ π`. -/ @[simps, implicit_reducible] @@ -434,7 +427,6 @@ theorem Fork.condition (t : Fork f g) : t.ι ≫ f = t.ι ≫ g := by theorem Cofork.condition (t : Cofork f g) : f ≫ t.π = g ≫ t.π := by rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right] -set_option backward.isDefEq.respectTransparency false in /-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the first map -/ theorem Fork.equalizer_ext (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) : @@ -445,7 +437,6 @@ theorem Fork.equalizer_ext (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ simp only [← Category.assoc]; exact congrArg (· ≫ f) h rw [s.app_one_eq_ι_comp_left, this] -set_option backward.isDefEq.respectTransparency false in /-- To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for the second map -/ theorem Cofork.coequalizer_ext (s : Cofork f g) {W : C} {k l : s.pt ⟶ W} @@ -538,7 +529,6 @@ def Fork.IsLimit.mk' {X Y : C} {f g : X ⟶ Y} (t : Fork f g) (create : ∀ s : Fork f g, { l // l ≫ t.ι = s.ι ∧ ∀ {m}, m ≫ t.ι = s.ι → m = l }) : IsLimit t := Fork.IsLimit.mk t (fun s => (create s).1) (fun s => (create s).2.1) fun s _ w => (create s).2.2 w -set_option backward.defeqAttrib.useBackward true in /-- This is a slightly more convenient method to verify that a cofork is a colimit cocone. It only asks for a proof of facts that carry any mathematical content -/ def Cofork.IsColimit.mk (t : Cofork f g) (desc : ∀ s : Cofork f g, t.pt ⟶ s.pt) @@ -610,7 +600,6 @@ theorem Cofork.IsColimit.homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Cofork f (Cofork.IsColimit.homIso ht _ k : Y ⟶ Z) ≫ q := (Category.assoc _ _ _).symm -set_option backward.defeqAttrib.useBackward true in /-- This is a helper construction that can be useful when verifying that a category has all equalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as `parallelPair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`, @@ -624,8 +613,6 @@ def Cone.ofFork {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map ri { app := fun X => t.π.app X ≫ eqToHom (by simp) naturality := by rintro _ _ (_ | _ | _) <;> simp [t.condition] } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- This is a helper construction that can be useful when verifying that a category has all coequalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as `parallelPair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`, @@ -649,7 +636,6 @@ theorem Cone.ofFork_π {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F theorem Cocone.ofCofork_ι {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right)) (j) : (Cocone.ofCofork t).ι.app j = eqToHom (by simp) ≫ t.ι.app j := rfl -set_option backward.defeqAttrib.useBackward true in /-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as `parallelPair (F.map left) (F.map right)` and a cone on `F`, we get a fork on `F.map left` and `F.map right`. -/ @@ -658,8 +644,6 @@ def Fork.ofCone {F : WalkingParallelPair ⥤ C} (t : Cone F) : Fork (F.map left) π := { app := fun X => t.π.app X ≫ eqToHom (by simp) naturality := by rintro _ _ (_ | _ | _) <;> simp } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as `parallelPair (F.map left) (F.map right)` and a cocone on `F`, we get a cofork on `F.map left` and `F.map right`. -/ @@ -687,7 +671,6 @@ theorem Cofork.π_precompose {f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parall {c : Cofork f' g'} : Cofork.π ((Cocone.precompose α).obj c) = α.app .one ≫ c.π := rfl -set_option backward.isDefEq.respectTransparency false in /-- Helper function for constructing morphisms between equalizer forks. -/ @[simps] @@ -709,13 +692,11 @@ def Fork.ext {s t : Fork f g} (i : s.pt ≅ t.pt) (w : i.hom ≫ t.ι = s.ι := hom := Fork.mkHom i.hom w inv := Fork.mkHom i.inv (by rw [← w, Iso.inv_hom_id_assoc]) -set_option backward.defeqAttrib.useBackward true in /-- Two forks of the form `ofι` are isomorphic whenever their `ι`'s are equal. -/ def ForkOfι.ext {P : C} {ι ι' : P ⟶ X} (w : ι ≫ f = ι ≫ g) (w' : ι' ≫ f = ι' ≫ g) (h : ι = ι') : Fork.ofι ι w ≅ Fork.ofι ι' w' := Fork.ext (Iso.refl _) (by simp [h]) -set_option backward.defeqAttrib.useBackward true in /-- Every fork is isomorphic to one of the form `Fork.of_ι _ _`. -/ @[simps!] def Fork.isoForkOfι (c : Fork f g) : c ≅ Fork.ofι c.ι c.condition := @@ -804,13 +785,11 @@ def Cofork.ext {s t : Cofork f g} (i : s.pt ≅ t.pt) (w : s.π ≫ i.hom = t.π hom := Cofork.mkHom i.hom w inv := Cofork.mkHom i.inv (by rw [Iso.comp_inv_eq, w]) -set_option backward.defeqAttrib.useBackward true in /-- Two coforks of the form `ofπ` are isomorphic whenever their `π`'s are equal. -/ def CoforkOfπ.ext {P : C} {π π' : Y ⟶ P} (w : f ≫ π = g ≫ π) (w' : f ≫ π' = g ≫ π') (h : π = π') : Cofork.ofπ π w ≅ Cofork.ofπ π' w' := Cofork.ext (Iso.refl _) (by simp [h]) -set_option backward.defeqAttrib.useBackward true in /-- Every cofork is isomorphic to one of the form `Cofork.ofπ _ _`. -/ def Cofork.isoCoforkOfπ (c : Cofork f g) : c ≅ Cofork.ofπ c.π c.condition := Cofork.ext (Iso.refl _) @@ -879,7 +858,6 @@ theorem equalizer.fork_π_app_zero : (equalizer.fork f g).π.app zero = equalize theorem equalizer.condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g := Fork.condition <| limit.cone <| parallelPair f g -set_option backward.defeqAttrib.useBackward true in /-- The equalizer built from `equalizer.ι f g` is limiting. -/ noncomputable def equalizerIsEqualizer : IsLimit (Fork.ofι (equalizer.ι f g) (equalizer.condition f g)) := @@ -934,17 +912,16 @@ section variable {f g} /-- The identity determines a cone on the equalizer diagram of `f` and `g` if `f = g`. -/ +@[implicit_reducible] def idFork (h : f = g) : Fork f g := Fork.ofι (𝟙 X) <| h ▸ rfl -set_option backward.isDefEq.respectTransparency.types false in /-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`. -/ def isLimitIdFork (h : f = g) : IsLimit (idFork h) := Fork.IsLimit.mk _ (fun s => Fork.ι s) (fun _ => Category.comp_id _) fun s m h => by convert! h exact (Category.comp_id _).symm -set_option backward.isDefEq.respectTransparency.types false in /-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ theorem isIso_limit_cone_parallelPair_of_eq (h₀ : f = g) {c : Fork f g} (h : IsLimit c) : IsIso c.ι := @@ -989,7 +966,6 @@ noncomputable def equalizer.isoSourceOfSelf : equalizer f f ≅ X := theorem equalizer.isoSourceOfSelf_hom : (equalizer.isoSourceOfSelf f).hom = equalizer.ι f f := rfl -set_option backward.isDefEq.respectTransparency false in @[simp] theorem equalizer.isoSourceOfSelf_inv : (equalizer.isoSourceOfSelf f).inv = equalizer.lift (𝟙 X) (by simp) := by @@ -1089,7 +1065,6 @@ theorem coequalizer.cofork_ι_app_one : (coequalizer.cofork f g).ι.app one = co theorem coequalizer.condition : f ≫ coequalizer.π f g = g ≫ coequalizer.π f g := Cofork.condition <| colimit.cocone <| parallelPair f g -set_option backward.defeqAttrib.useBackward true in /-- The cofork built from `coequalizer.π f g` is colimiting. -/ noncomputable def coequalizerIsCoequalizer : IsColimit (Cofork.ofπ (coequalizer.π f g) (coequalizer.condition f g)) := @@ -1108,7 +1083,6 @@ theorem coequalizer.π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : coequalizer.π f g ≫ coequalizer.desc k h = k := colimit.ι_desc _ _ -set_option backward.isDefEq.respectTransparency false in theorem coequalizer.π_colimMap_desc {X' Y' Z : C} (f' g' : X' ⟶ Y') [HasCoequalizer f' g'] (p : X ⟶ X') (q : Y ⟶ Y') (wf : f ≫ q = p ≫ f') (wg : g ≫ q = p ≫ g') (h : Y' ⟶ Z) (wh : f' ≫ h = g' ≫ h) : @@ -1154,17 +1128,16 @@ section variable {f g} /-- The identity determines a cocone on the coequalizer diagram of `f` and `g`, if `f = g`. -/ +@[implicit_reducible] def idCofork (h : f = g) : Cofork f g := Cofork.ofπ (𝟙 Y) <| h ▸ rfl -set_option backward.isDefEq.respectTransparency.types false in /-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`. -/ def isColimitIdCofork (h : f = g) : IsColimit (idCofork h) := Cofork.IsColimit.mk _ (fun s => Cofork.π s) (fun _ => Category.id_comp _) fun s m h => by convert! h exact (Category.id_comp _).symm -set_option backward.isDefEq.respectTransparency.types false in /-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/ theorem isIso_colimit_cocone_parallelPair_of_eq (h₀ : f = g) {c : Cofork f g} (h : IsColimit c) : IsIso c.π := @@ -1206,7 +1179,6 @@ instance coequalizer.π_of_self : IsIso (coequalizer.π f f) := noncomputable def coequalizer.isoTargetOfSelf : coequalizer f f ≅ Y := (asIso (coequalizer.π f f)).symm -set_option backward.isDefEq.respectTransparency false in @[simp] theorem coequalizer.isoTargetOfSelf_hom : (coequalizer.isoTargetOfSelf f).hom = coequalizer.desc (𝟙 Y) (by simp) := by @@ -1235,7 +1207,6 @@ theorem equalizerComparison_comp_π [HasEqualizer f g] [HasEqualizer (G.map f) ( equalizerComparison f g G ≫ equalizer.ι (G.map f) (G.map g) = G.map (equalizer.ι f g) := equalizer.lift_ι _ _ -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem map_lift_equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : h ≫ f = h ≫ g) : @@ -1255,7 +1226,6 @@ theorem ι_comp_coequalizerComparison [HasCoequalizer f g] [HasCoequalizer (G.ma coequalizer.π _ _ ≫ coequalizerComparison f g G = G.map (coequalizer.π _ _) := coequalizer.π_desc _ _ -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem coequalizerComparison_map_desc [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) : @@ -1327,7 +1297,6 @@ def splitMonoOfEqualizer {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : f ≫ r ≫ variable {C f g} -set_option backward.isDefEq.respectTransparency false in /-- The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer. -/ def isEqualizerCompMono {c : Fork f g} (i : IsLimit c) {Z : C} (h : Y ⟶ Z) [hm : Mono h] : have : Fork.ι c ≫ f ≫ h = Fork.ι c ≫ g ≫ h := by @@ -1348,7 +1317,6 @@ theorem hasEqualizer_comp_mono [HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [Mono h] ⟨⟨{ cone := _ isLimit := isEqualizerCompMono (limit.isLimit _) h }⟩⟩ -set_option backward.isDefEq.respectTransparency false in /-- An equalizer of an idempotent morphism and the identity is split mono. -/ @[simps] def splitMonoOfIdempotentOfIsLimitFork {X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Fork (𝟙 X) f} @@ -1406,7 +1374,6 @@ def splitEpiOfCoequalizer {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s variable {C f g} -set_option backward.isDefEq.respectTransparency false in /-- The cofork obtained by precomposing a coequalizer cofork with an epimorphism is a coequalizer. -/ def isCoequalizerEpiComp {c : Cofork f g} (i : IsColimit c) {W : C} (h : W ⟶ X) [hm : Epi h] : @@ -1428,7 +1395,6 @@ theorem hasCoequalizer_epi_comp [HasCoequalizer f g] {W : C} (h : W ⟶ X) [Epi variable (C f g) -set_option backward.isDefEq.respectTransparency false in /-- A coequalizer of an idempotent morphism and the identity is split epi. -/ @[simps] def splitEpiOfIdempotentOfIsColimitCofork {X : C} {f : X ⟶ X} (hf : f ≫ f = f) {c : Cofork (𝟙 X) f} diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean index 2d149581f8a..9af0efb66f7 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean @@ -39,7 +39,6 @@ variable {C : Type u₁} [Category.{v₁} C] #adaptation_note /-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in /-- Construct a cone for the empty diagram given an object. -/ @[simps, implicit_reducible] def asEmptyCone (X : C) : Cone (Functor.empty.{0} C) := @@ -49,9 +48,8 @@ def asEmptyCone (X : C) : Cone (Functor.empty.{0} C) := #adaptation_note /-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in /-- Construct a cocone for the empty diagram given an object. -/ -@[simps] +@[implicit_reducible, simps] def asEmptyCocone (X : C) : Cocone (Functor.empty.{0} C) := { pt := X ι := @@ -80,7 +78,6 @@ def isTerminalEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (Y : C) : dsimp [Function.RightInverse, Function.LeftInverse] subsingleton -set_option backward.defeqAttrib.useBackward true in /-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y` (as an instance). -/ def IsTerminal.ofUnique (Y : C) [h : ∀ X : C, Unique (X ⟶ Y)] : IsTerminal Y where @@ -98,7 +95,6 @@ def IsTerminal.ofUniqueHom {Y : C} (h : ∀ X : C, X ⟶ Y) (uniq : ∀ (X : C) def isTerminalTop {α : Type*} [Preorder α] [OrderTop α] : IsTerminal (⊤ : α) := IsTerminal.ofUnique _ -set_option backward.isDefEq.respectTransparency.types false in /-- Transport a term of type `IsTerminal` across an isomorphism. -/ def IsTerminal.ofIso {Y Z : C} (hY : IsTerminal Y) (i : Y ≅ Z) : IsTerminal Z := IsLimit.ofIsoLimit hY @@ -125,7 +121,6 @@ def isInitialEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) : left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton] right_inv := by grind -set_option backward.defeqAttrib.useBackward true in /-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y` (as an instance). -/ def IsInitial.ofUnique (X : C) [h : ∀ Y : C, Unique (X ⟶ Y)] : IsInitial X where @@ -143,7 +138,6 @@ def IsInitial.ofUniqueHom {X : C} (h : ∀ Y : C, X ⟶ Y) (uniq : ∀ (Y : C) ( def isInitialBot {α : Type*} [Preorder α] [OrderBot α] : IsInitial (⊥ : α) := IsInitial.ofUnique _ -set_option backward.isDefEq.respectTransparency.types false in /-- Transport a term of type `IsInitial` across an isomorphism. -/ def IsInitial.ofIso {X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y := IsColimit.ofIsoColimit hX @@ -344,10 +338,9 @@ theorem InitialMonoClass.of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerm variable {J : Type u} [Category.{v} J] -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cone for `J`. In `limitOfDiagramInitial` we show it is a limit cone. -/ -@[simps] +@[implicit_reducible, simps] def coneOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) : Cone F where pt := F.obj X π := @@ -356,8 +349,6 @@ def coneOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) : Cone F where dsimp rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')] } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given an initial object of `J`, show the cone `coneOfDiagramInitial` is a limit. -/ def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) : @@ -368,12 +359,10 @@ def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) : simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)] simp -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cone for `J`, provided that the morphisms in the diagram are isomorphisms. In `limitOfDiagramTerminal` we show it is a limit cone. -/ -@[simps] +@[implicit_reducible, simps] def coneOfDiagramTerminal {X : J} (hX : IsTerminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cone F where pt := F.obj X @@ -385,18 +374,15 @@ def coneOfDiagramTerminal {X : J} (hX : IsTerminal X) (F : J ⥤ C) simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.id_comp, ← F.map_comp, hX.hom_ext (hX.from i) (f ≫ hX.from j)] } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given a terminal object of `J` and that the morphisms in the diagram are isomorphisms, show the cone `coneOfDiagramTerminal` is a limit. -/ def limitOfDiagramTerminal {X : J} (hX : IsTerminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsLimit (coneOfDiagramTerminal hX F) where lift S := S.π.app _ -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cocone for `J`. In `colimitOfDiagramTerminal` we show it is a colimit cocone. -/ -@[simps] +@[implicit_reducible, simps] def coconeOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) : Cocone F where pt := F.obj X ι := @@ -405,8 +391,6 @@ def coconeOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) : Cocone F dsimp rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)] } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, show the cocone `coconeOfDiagramTerminal` is a colimit. -/ def colimitOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) : @@ -420,12 +404,10 @@ lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : Is change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom infer_instance -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cocone for `J`, provided that the morphisms in the diagram are isomorphisms. In `colimitOfDiagramInitial` we show it is a colimit cocone. -/ -@[simps] +@[implicit_reducible, simps] def coconeOfDiagramInitial {X : J} (hX : IsInitial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cocone F where pt := F.obj X @@ -437,8 +419,6 @@ def coconeOfDiagramInitial {X : J} (hX : IsInitial X) (F : J ⥤ C) simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.comp_id, ← F.map_comp, hX.hom_ext (hX.to i ≫ f) (hX.to j)] } -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- From a functor `F : J ⥤ C`, given an initial object of `J` and that the morphisms in the diagram are isomorphisms, show the cone `coconeOfDiagramInitial` is a colimit. -/ def colimitOfDiagramInitial {X : J} (hX : IsInitial X) (F : J ⥤ C) @@ -493,7 +473,6 @@ namespace Functor open Limits variable (C : Type*) [Category* C] {D : Type*} [Category* D] -set_option backward.defeqAttrib.useBackward true in /-- The constant functor returning a specific terminal object is indeed terminal. -/ def isTerminalConst {X : D} (hX : IsTerminal X) : IsTerminal ((Functor.const C).obj X) := @@ -503,7 +482,6 @@ def isTerminalConst {X : D} (hX : IsTerminal X) : lemma isTerminalConst_from_app {X : D} (hX : IsTerminal X) (F : C ⥤ D) (Y : C) : ((isTerminalConst C hX).from F).app Y = hX.from (F.obj Y) := rfl -set_option backward.defeqAttrib.useBackward true in /-- The constant functor returning a specific initial object is indeed initial. -/ def isInitialConst {X : D} (hX : IsInitial X) : IsInitial ((Functor.const C).obj X) := diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean index 8985bf1198f..277c61c75b7 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean @@ -228,13 +228,10 @@ lemma Sigma.hom_ext {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f (h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂) : g₁ = g₂ := colimit.hom_ext (fun ⟨j⟩ => h j) -set_option backward.defeqAttrib.useBackward true in /-- The fan constructed of the projections from the product is limiting. -/ def productIsProduct (f : β → C) [HasProduct f] : IsLimit (Fan.mk _ (Pi.π f)) := IsLimit.ofIsoLimit (limit.isLimit (Discrete.functor f)) (Cone.ext (Iso.refl _)) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- The cofan constructed of the inclusions from the coproduct is colimiting. -/ def coproductIsCoproduct (f : β → C) [HasCoproduct f] : IsColimit (Cofan.mk _ (Sigma.ι f)) := IsColimit.ofIsoColimit (colimit.isColimit (Discrete.functor f)) (Cocone.ext (Iso.refl _)) @@ -256,7 +253,6 @@ theorem Sigma.eqToHom_comp_ι {J : Type*} (f : J → C) [HasCoproduct f] {j j' : abbrev Pi.lift {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) : P ⟶ ∏ᶜ f := limit.lift _ (Fan.mk P p) -set_option backward.isDefEq.respectTransparency false in @[reassoc, elementwise] theorem Pi.lift_π {β : Type w} {f : β → C} [HasProduct f] {P : C} (p : ∀ b, P ⟶ f b) (b : β) : Pi.lift p ≫ Pi.π f b = p b := by @@ -282,13 +278,11 @@ lemma Fan.nonempty_isLimit_iff_isIso_piLift {f : β → C} [HasProduct f] (c : F abbrev Sigma.desc {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) : ∐ f ⟶ P := colimit.desc _ (Cofan.mk P p) -set_option backward.isDefEq.respectTransparency false in @[reassoc] theorem Sigma.ι_desc {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : ∀ b, f b ⟶ P) (b : β) : Sigma.ι f b ≫ Sigma.desc p = p b := by simp only [colimit.ι_desc, Cofan.mk_ι_app] -set_option backward.isDefEq.respectTransparency false in instance {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc (fun a ↦ Sigma.ι f a)) := by convert! IsIso.id _ ext @@ -313,8 +307,6 @@ lemma Cofan.nonempty_isColimit_iff_isIso_sigmaDesc {f : β → C} [HasCoproduct @[deprecated (since := "2026-01-21")] alias Cofan.isColimit_iff_isIso_sigmaDesc := Cofan.nonempty_isColimit_iff_isIso_sigmaDesc -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- A coproduct of coproducts is a coproduct -/ def Cofan.isColimitTrans {X : α → C} (c : Cofan X) (hc : IsColimit c) {β : α → Type*} {Y : (a : α) → β a → C} (π : (a : α) → (b : β a) → Y a b ⟶ X a) @@ -338,7 +330,6 @@ from a family of morphisms between the factors. def Pi.map {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g := limMap (Discrete.natTrans fun X => p X.as) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp), elementwise nosimp] lemma Pi.map_π {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) (b : β) : Pi.map p ≫ Pi.π g b = Pi.π f b ≫ p b := by simp [Pi.map] @@ -352,8 +343,6 @@ lemma Pi.map_comp_map {f g h : α → C} [HasProduct f] [HasProduct g] [HasProdu Pi.map q ≫ Pi.map q' = Pi.map (fun a => q a ≫ q' a) := by ext; simp -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in instance Pi.map_mono {f g : β → C} [HasProduct f] [HasProduct g] (p : ∀ b, f b ⟶ g b) [∀ i, Mono (p i)] : Mono <| Pi.map p := @Limits.limMap_mono _ _ _ _ (Discrete.functor f) (Discrete.functor g) _ _ @@ -434,7 +423,6 @@ def Pi.cone : Cone X where π := Discrete.natTrans (fun _ => Pi.π _ _) set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The cone `Pi.cone X` is a limit cone. -/ def productIsProduct' : IsLimit (Pi.cone X) where @@ -472,7 +460,6 @@ def Sigma.map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ∐ f ⟶ ∐ g := colimMap (Discrete.natTrans fun X => p X.as) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] lemma Sigma.ι_map {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) (b : β) : Sigma.ι f b ≫ Sigma.map p = p b ≫ Sigma.ι g b := by simp [Sigma.map] @@ -486,8 +473,6 @@ lemma Sigma.map_comp_map {f g h : α → C} [HasCoproduct f] [HasCoproduct g] [H Sigma.map q ≫ Sigma.map q' = Sigma.map (fun a => q a ≫ q' a) := by ext; simp -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in instance Sigma.map_epi {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : ∀ b, f b ⟶ g b) [∀ i, Epi (p i)] : Epi <| Sigma.map p := @Limits.colimMap_epi _ _ _ _ (Discrete.functor f) (Discrete.functor g) _ _ @@ -571,7 +556,6 @@ def Sigma.cocone : Cocone X where ι := Discrete.natTrans (fun _ => Sigma.ι (fun j ↦ X.obj ⟨j⟩) _) set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The cocone `Sigma.cocone X` is a colimit cocone. -/ def coproductIsCoproduct' : IsColimit (Sigma.cocone X) where @@ -620,8 +604,6 @@ def Sigma.whiskerEquiv {J K : Type*} {f : J → C} {g : K → C} (e : J ≃ K) ( hom := Sigma.map' e fun j => (w j).inv inv := Sigma.map' e.symm fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ᶜ g i] : HasProduct fun p : Σ i, f i => g p.1 p.2 where @@ -631,7 +613,6 @@ instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) (by simp) (by intro s (m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i)) w; aesop (add norm simp Sigma.forall)) } -set_option backward.isDefEq.respectTransparency false in /-- An iterated product is a product over a sigma type. -/ @[simps] def piPiIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) @@ -640,8 +621,6 @@ def piPiIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) hom := Pi.lift fun ⟨i, x⟩ => Pi.π _ i ≫ Pi.π _ x inv := Pi.lift fun i => Pi.lift fun x => Pi.π _ (⟨i, x⟩ : Σ i, f i) -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasCoproduct (g i)] [HasCoproduct fun i => ∐ g i] : HasCoproduct fun p : Σ i, f i => g p.1 p.2 where @@ -653,7 +632,6 @@ instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) (by simp) (by intro s (m : (∐ fun i ↦ ∐ g i) ⟶ _) w; aesop_cat (add norm simp Sigma.forall)) } -set_option backward.isDefEq.respectTransparency false in /-- An iterated coproduct is a coproduct over a sigma type. -/ @[simps] def sigmaSigmaIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) @@ -678,7 +656,6 @@ theorem piComparison_comp_π [HasProduct f] [HasProduct fun b => G.obj (f b)] (b piComparison G f ≫ Pi.π _ b = G.map (Pi.π f b) := limit.lift_π _ (Discrete.mk b) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C) (g : ∀ j, P ⟶ f j) : G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j) := by @@ -697,7 +674,6 @@ theorem ι_comp_sigmaComparison [HasCoproduct f] [HasCoproduct fun b => G.obj (f Sigma.ι _ b ≫ sigmaComparison G f = G.map (Sigma.ι f b) := colimit.ι_desc _ (Discrete.mk b) -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C) (g : ∀ j, f j ⟶ P) : @@ -705,16 +681,12 @@ theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj ( ext j simp only [ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc, Cofan.mk_ι_app] -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- `F.mapCone c` being limiting is the same as the induced fan being limiting. -/ def Fan.isLimitMapConeEquiv (F : C ⥤ D) {ι : Type*} (X : ι → C) (c : Fan X) : IsLimit (F.mapCone c) ≃ IsLimit (Fan.mk _ fun i ↦ F.map (c.proj i)) := (IsLimit.postcomposeHomEquiv Discrete.natIsoFunctor (F.mapCone c)).symm.trans <| IsLimit.equivIsoLimit (Cone.ext (Iso.refl _)) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- `F.mapCocone c` being colimiting is the same as the induced cofan being colimiting. -/ def Cofan.isColimitMapCoconeEquiv (F : C ⥤ D) {ι : Type*} (X : ι → C) (c : Cofan X) : IsColimit (F.mapCocone c) ≃ IsColimit (Cofan.mk _ fun i ↦ F.map (c.inj i)) := @@ -771,13 +743,11 @@ instance (priority := 100) hasCoproductsOfShape_of_hasCoproducts [HasCoproducts. open Opposite in /-- The functor sending `(X, n)` to the product of copies of `X` indexed by `n`. -/ -@[simps] +@[implicit_reducible, simps] def piConst [Limits.HasProducts.{w} C] : C ⥤ Type wᵒᵖ ⥤ C where obj X := { obj n := ∏ᶜ fun _ : (unop n :) ↦ X, map f := Limits.Pi.map' f.unop fun _ ↦ 𝟙 _ } map f := { app n := Limits.Pi.map fun _ ↦ f } -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- `n ↦ ∏ₙ X` is left adjoint to `Hom(-, X)`. -/ def piConstAdj [Limits.HasProducts.{v} C] (X : C) : (piConst.obj X).rightOp ⊣ yoneda.obj X where @@ -788,13 +758,11 @@ def piConstAdj [Limits.HasProducts.{v} C] (X : C) : left_triangle_components _ := by apply Quiver.Hom.unop_inj; cat_disch /-- The functor sending `(X, n)` to the coproduct of copies of `X` indexed by `n`. -/ -@[simps] +@[implicit_reducible, simps] def sigmaConst [Limits.HasCoproducts.{w} C] : C ⥤ Type w ⥤ C where obj X := { obj n := ∐ fun _ : n ↦ X, map f := Limits.Sigma.map' f fun _ ↦ 𝟙 _ } map f := { app n := Limits.Sigma.map fun _ ↦ f } -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- `n ↦ ∐ₙ X` is left adjoint to `Hom(X, -)`. -/ def sigmaConstAdj [Limits.HasCoproducts.{v} C] (X : C) : sigmaConst.obj X ⊣ coyoneda.obj (Opposite.op X) where @@ -808,8 +776,6 @@ def sigmaConstAdj [Limits.HasCoproducts.{v} C] (X : C) : section Unique -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- The limit cone for the product over an index type with exactly one term. -/ @[simps] def limitConeOfUnique [Unique β] (f : β → C) : LimitCone (Discrete.functor f) where @@ -848,8 +814,6 @@ lemma productUniqueIso_inv_π [Unique β] (f : β → C) (b : β) : @[deprecated (since := "2026-06-30")] alias productUniqueIso_inv := productUniqueIso_inv_π -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- Any isomorphism is the projection from a single object product. -/ def Fan.isLimitMkOfUnique {X Y : C} (e : X ≅ Y) (J : Type*) [Unique J] : IsLimit (Fan.mk X fun _ : J ↦ e.hom) := by @@ -858,8 +822,6 @@ def Fan.isLimitMkOfUnique {X Y : C} (e : X ≅ Y) (J : Type*) [Unique J] : simp · simpa [← cancel_mono e.hom] using hm default -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- The colimit cocone for the coproduct over an index type with exactly one term. -/ @[simps] def colimitCoconeOfUnique [Unique β] (f : β → C) : ColimitCocone (Discrete.functor f) where @@ -900,8 +862,6 @@ lemma ι_coproductUniqueIso_hom [Unique β] (f : β → C) (b : β) : @[deprecated (since := "2026-06-30")] alias coproductUniqueIso_hom := ι_coproductUniqueIso_hom -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- Any isomorphism is the projection from a single object product. -/ def Cofan.isColimitMkOfUnique {X Y : C} (e : X ≅ Y) (J : Type*) [Unique J] : IsColimit (Cofan.mk Y fun _ : J ↦ e.hom) := by @@ -968,7 +928,6 @@ theorem Sigma.ι_reindex_hom (b : β) : erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc] all_goals { simp } -set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] theorem Sigma.ι_reindex_inv (b : β) : Sigma.ι f (ε b) ≫ (Sigma.reindex ε f).inv = Sigma.ι (f ∘ ε) b := by simp [Iso.comp_inv_eq] @@ -987,13 +946,11 @@ section variable {J : Type u₂} [Category.{v₂} J] (F : J ⥤ C) -set_option backward.isDefEq.respectTransparency false in instance [HasLimit F] [HasProduct F.obj] : Mono (Pi.lift (limit.π F)) where right_cancellation _ _ h := by refine limit.hom_ext fun j => ?_ simpa using h =≫ Pi.π _ j -set_option backward.isDefEq.respectTransparency false in instance [HasColimit F] [HasCoproduct F.obj] : Epi (Sigma.desc (colimit.ι F)) where left_cancellation _ _ h := by refine colimit.hom_ext fun j => ?_ @@ -1026,8 +983,6 @@ section Fubini variable {ι ι' : Type*} {X : ι → ι' → C} -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- A product over products is a product indexed by a product. -/ def Fan.IsLimit.prod (c : ∀ i : ι, Fan (fun j : ι' ↦ X i j)) (hc : ∀ i : ι, IsLimit (c i)) (c' : Fan (fun i : ι ↦ (c i).pt)) (hc' : IsLimit c') : @@ -1038,8 +993,6 @@ def Fan.IsLimit.prod (c : ∀ i : ι, Fan (fun j : ι' ↦ X i j)) (hc : ∀ i : · refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_ exact Fan.IsLimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j)) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in /-- A coproduct over coproducts is a coproduct indexed by a product. -/ def Cofan.IsColimit.prod (c : ∀ i : ι, Cofan (fun j : ι' ↦ X i j)) (hc : ∀ i : ι, IsColimit (c i)) (c' : Cofan (fun i : ι ↦ (c i).pt)) (hc' : IsColimit c') : @@ -1074,7 +1027,6 @@ def piEquivalenceFunctorDiscreteCompLim [HasProductsOfShape α C] : (piEquivalenceFunctorDiscrete α C).functor ⋙ lim ≅ Pi.functor _ := NatIso.ofComponents fun _ ↦ Iso.refl _ -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in @[reassoc] lemma piEquivalenceFunctorDiscreteCompLim_comp_functorπ [HasProductsOfShape α C] (a : α) : @@ -1083,7 +1035,6 @@ lemma piEquivalenceFunctorDiscreteCompLim_comp_functorπ [HasProductsOfShape α (piEquivalenceFunctorDiscreteCompEvaluationIso _ _).hom := by cat_disch -set_option backward.defeqAttrib.useBackward true in attribute [local simp] Functor.pi in /-- The `∏ᶜ` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic to the constant functor with value `∏ᶜ X`. -/ @@ -1117,7 +1068,6 @@ def piEquivalenceFunctorDiscreteCompColim [HasCoproductsOfShape α C] : (piEquivalenceFunctorDiscrete α C).functor ⋙ colim ≅ Sigma.functor _ := NatIso.ofComponents fun _ ↦ Iso.refl _ -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in @[reassoc] lemma piEquivalenceFunctorDiscreteCompColim_comp_functorι [HasCoproductsOfShape α C] (a : α) : @@ -1129,7 +1079,6 @@ lemma piEquivalenceFunctorDiscrete_functor_comp_colim [HasCoproductsOfShape α C (piEquivalenceFunctorDiscrete α C).functor ⋙ colim = Sigma.functor _ := rfl -set_option backward.defeqAttrib.useBackward true in attribute [local simp] Functor.pi in /-- The `∐` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic to the constant functor with value `∐ X`. -/ diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean index 8122b68b9f2..71e5a10957e 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean @@ -118,12 +118,10 @@ abbrev terminal.from [HasTerminal C] (P : C) : P ⟶ ⊤_ C := abbrev initial.to [HasInitial C] (P : C) : ⊥_ C ⟶ P := colimit.desc (Functor.empty C) (asEmptyCocone P) -set_option backward.defeqAttrib.useBackward true in /-- A terminal object is terminal. -/ def terminalIsTerminal [HasTerminal C] : IsTerminal (⊤_ C) where lift _ := terminal.from _ -set_option backward.defeqAttrib.useBackward true in /-- An initial object is initial. -/ def initialIsInitial [HasInitial C] : IsInitial (⊥_ C) where desc _ := initial.to _ @@ -178,7 +176,6 @@ theorem hasTerminal_of_hasInitial_op [HasInitial Cᵒᵖ] : HasTerminal C := theorem hasInitial_of_hasTerminal_op [HasTerminal Cᵒᵖ] : HasInitial C := (initialUnopOfTerminal terminalIsTerminal).hasInitial -set_option backward.defeqAttrib.useBackward true in instance {J : Type*} [Category* J] {C : Type*} [Category* C] [HasTerminal C] : HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C)) := HasLimit.mk @@ -187,7 +184,6 @@ instance {J : Type*} [Category* J] {C : Type*} [Category* C] [HasTerminal C] : π := { app := fun _ => terminal.from _ } } isLimit := { lift := fun _ => terminal.from _ } } -set_option backward.defeqAttrib.useBackward true in /-- The limit of the constant `⊤_ C` functor is `⊤_ C`. -/ @[simps hom] def limitConstTerminal {J : Type*} [Category* J] {C : Type*} [Category* C] [HasTerminal C] : @@ -198,14 +194,12 @@ def limitConstTerminal {J : Type*} [Category* J] {C : Type*} [Category* C] [HasT { pt := ⊤_ C π := { app := fun _ => terminal.from _ } } -set_option backward.defeqAttrib.useBackward true in @[reassoc (attr := simp)] theorem limitConstTerminal_inv_π {J : Type*} [Category* J] {C : Type*} [Category* C] [HasTerminal C] {j : J} : limitConstTerminal.inv ≫ limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j = terminal.from _ := by cat_disch -set_option backward.defeqAttrib.useBackward true in instance {J : Type*} [Category* J] {C : Type*} [Category* C] [HasInitial C] : HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) := HasColimit.mk @@ -214,7 +208,6 @@ instance {J : Type*} [Category* J] {C : Type*} [Category* C] [HasInitial C] : ι := { app := fun _ => initial.to _ } } isColimit := { desc := fun _ => initial.to _ } } -set_option backward.defeqAttrib.useBackward true in /-- The colimit of the constant `⊥_ C` functor is `⊥_ C`. -/ @[simps inv] def colimitConstInitial {J : Type*} [Category* J] {C : Type*} [Category* C] [HasInitial C] : @@ -225,7 +218,6 @@ def colimitConstInitial {J : Type*} [Category* J] {C : Type*} [Category* C] [Has ι := { app := fun _ => initial.to _ } } inv := initial.to _ -set_option backward.defeqAttrib.useBackward true in @[reassoc (attr := simp)] theorem ι_colimitConstInitial_hom {J : Type*} [Category* J] {C : Type*} [Category* C] [HasInitial C] {j : J} : @@ -314,7 +306,6 @@ abbrev colimitOfInitial (F : J ⥤ C) [HasInitial J] [∀ (i j : J) (f : i ⟶ j IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitOfDiagramInitial initialIsInitial _) -set_option backward.isDefEq.respectTransparency false in /-- If `j` is initial in the index category, then the map `limit.π F j` is an isomorphism. -/ theorem isIso_π_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit F] : @@ -324,7 +315,6 @@ theorem isIso_π_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit instance isIso_π_initial [HasInitial J] (F : J ⥤ C) : IsIso (limit.π F (⊥_ J)) := isIso_π_of_isInitial initialIsInitial F -set_option backward.isDefEq.respectTransparency false in theorem isIso_π_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasLimit F] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F j) := ⟨⟨limit.lift _ (coneOfDiagramTerminal I F), by ext; simp, by simp⟩⟩ @@ -333,7 +323,6 @@ instance isIso_π_terminal [HasTerminal J] (F : J ⥤ C) [∀ (i j : J) (f : i IsIso (limit.π F (⊤_ J)) := isIso_π_of_isTerminal terminalIsTerminal F -set_option backward.isDefEq.respectTransparency false in /-- If `j` is terminal in the index category, then the map `colimit.ι F j` is an isomorphism. -/ theorem isIso_ι_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColimit F] : @@ -343,8 +332,6 @@ theorem isIso_ι_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColi instance isIso_ι_terminal [HasTerminal J] (F : J ⥤ C) : IsIso (colimit.ι F (⊤_ J)) := isIso_ι_of_isTerminal terminalIsTerminal F -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in theorem isIso_ι_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasColimit F] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F j) := ⟨⟨colimit.desc _ (coconeOfDiagramInitial I F), by diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean index 23a505d37e2..b4547cad3b4 100644 --- a/Mathlib/CategoryTheory/NatIso.lean +++ b/Mathlib/CategoryTheory/NatIso.lean @@ -49,7 +49,7 @@ namespace Iso /-- The application of a natural isomorphism to an object. We put this definition in a different namespace, so that we can use `α.app` -/ -@[simps (attr := grind =)] +@[implicit_reducible, simps (attr := grind =)] def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X where hom := α.hom.app X diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 3433aa65b65..59d0dbd4c2d 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/Mathlib/CategoryTheory/Opposites.lean @@ -135,18 +135,17 @@ section variable (C) /-- The functor from the double-opposite of a category to the underlying category. -/ -@[simps] +@[implicit_reducible, simps] def unopUnop : Cᵒᵖᵒᵖ ⥤ C where obj X := unop (unop X) map f := f.unop.unop /-- The functor from a category to its double-opposite. -/ -@[simps] +@[implicit_reducible, simps] def opOp : C ⥤ Cᵒᵖᵒᵖ where obj X := op (op X) map f := f.op.op -set_option backward.defeqAttrib.useBackward true in /-- The double opposite category is equivalent to the original. -/ @[simps] def opOpEquivalence : Cᵒᵖᵒᵖ ≌ C where @@ -218,13 +217,11 @@ protected def unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D where obj X := unop (F.obj (op X)) map f := (F.map f.op).unop -set_option backward.defeqAttrib.useBackward true in /-- The isomorphism between `F.op.unop` and `F`. -/ @[simps!] def opUnopIso (F : C ⥤ D) : F.op.unop ≅ F := NatIso.ofComponents fun _ => Iso.refl _ -set_option backward.defeqAttrib.useBackward true in /-- The isomorphism between `F.unop.op` and `F`. -/ @[simps!] def unopOpIso (F : Cᵒᵖ ⥤ Dᵒᵖ) : F.unop.op ≅ F := @@ -234,7 +231,7 @@ variable (C D) /-- Taking the opposite of a functor is functorial. -/ -@[simps] +@[implicit_reducible, simps] def opHom : (C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ where obj F := (unop F).op map α := @@ -243,7 +240,7 @@ def opHom : (C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ where /-- Take the "unopposite" of a functor is functorial. -/ -@[simps] +@[implicit_reducible, simps] def opInv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ where obj F := op F.unop map α := @@ -281,7 +278,7 @@ end Compositions Another variant of the opposite of functor, turning a functor `C ⥤ Dᵒᵖ` into a functor `Cᵒᵖ ⥤ D`. In informal mathematics no distinction is made. -/ -@[simps] +@[implicit_reducible, simps] protected def leftOp (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D where obj X := unop (F.obj (unop X)) map f := (F.map f.unop).unop @@ -290,7 +287,7 @@ protected def leftOp (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D where Another variant of the opposite of functor, turning a functor `Cᵒᵖ ⥤ D` into a functor `C ⥤ Dᵒᵖ`. In informal mathematics no distinction is made. -/ -@[simps] +@[implicit_reducible, simps] protected def rightOp (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ where obj X := op (F.obj (op X)) map f := (F.map f.op).op @@ -298,20 +295,16 @@ protected def rightOp (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ where lemma rightOp_map_unop {F : Cᵒᵖ ⥤ D} {X Y} (f : X ⟶ Y) : (F.rightOp.map f).unop = F.map f.op := rfl -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in instance {F : C ⥤ D} [Full F] : Full F.op where map_surjective f := ⟨(F.preimage f.unop).op, by simp⟩ instance {F : C ⥤ D} [Faithful F] : Faithful F.op where map_injective h := Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h) -set_option backward.defeqAttrib.useBackward true in /-- The opposite of a fully faithful functor is fully faithful. -/ protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where preimage {X Y} f := .op <| hF.preimage f.unop -set_option backward.defeqAttrib.useBackward true in /-- A functor is fully faithful when its opposite is fully faithful. -/ protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) : F.unop.FullyFaithful where @@ -325,23 +318,17 @@ instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp instance leftOp_faithful {F : C ⥤ Dᵒᵖ} [Faithful F] : Faithful F.leftOp where map_injective h := Quiver.Hom.unop_inj (map_injective F (Quiver.Hom.unop_inj h)) -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in instance rightOp_full {F : Cᵒᵖ ⥤ D} [Full F] : Full F.rightOp where map_surjective f := ⟨(F.preimage f.unop).unop, by simp⟩ -set_option backward.isDefEq.respectTransparency.types false in -set_option backward.defeqAttrib.useBackward true in instance leftOp_full {F : C ⥤ Dᵒᵖ} [Full F] : Full F.leftOp where map_surjective f := ⟨(F.preimage f.op).op, by simp⟩ -set_option backward.defeqAttrib.useBackward true in /-- The opposite of a fully faithful functor is fully faithful. -/ protected def FullyFaithful.leftOp {F : C ⥤ Dᵒᵖ} (hF : F.FullyFaithful) : F.leftOp.FullyFaithful where preimage {X Y} f := .op <| hF.preimage f.op -set_option backward.defeqAttrib.useBackward true in /-- The opposite of a fully faithful functor is fully faithful. -/ protected def FullyFaithful.rightOp {F : Cᵒᵖ ⥤ D} (hF : F.FullyFaithful) : F.rightOp.FullyFaithful where @@ -372,13 +359,11 @@ def leftOpId : (𝟭 Cᵒᵖ).leftOp ≅ unopUnop C := Iso.refl _ end -set_option backward.defeqAttrib.useBackward true in /-- The isomorphism between `F.leftOp.rightOp` and `F`. -/ @[simps!] def leftOpRightOpIso (F : C ⥤ Dᵒᵖ) : F.leftOp.rightOp ≅ F := NatIso.ofComponents fun _ => Iso.refl _ -set_option backward.defeqAttrib.useBackward true in /-- The isomorphism between `F.rightOp.leftOp` and `F`. -/ @[simps!] def rightOpLeftOpIso (F : Cᵒᵖ ⥤ D) : F.rightOp.leftOp ≅ F := @@ -402,9 +387,8 @@ section variable {F G : C ⥤ D} -set_option backward.defeqAttrib.useBackward true in /-- The opposite of a natural transformation. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def op (α : F ⟶ G) : G.op ⟶ F.op where app X := (α.app (unop X)).op naturality X Y f := Quiver.Hom.unop_inj (by simp) @@ -418,23 +402,20 @@ theorem op_comp {H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.op (α ≫ β) = NatTrans.op β ≫ NatTrans.op α := rfl -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma op_whiskerRight {E : Type*} [Category* E] {H : D ⥤ E} (α : F ⟶ G) : NatTrans.op (whiskerRight α H) = (Functor.opComp _ _).hom ≫ whiskerRight (NatTrans.op α) H.op ≫ (Functor.opComp _ _).inv := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma op_whiskerLeft {E : Type*} [Category* E] {H : E ⥤ C} (α : F ⟶ G) : NatTrans.op (whiskerLeft H α) = (Functor.opComp _ _).hom ≫ whiskerLeft H.op (NatTrans.op α) ≫ (Functor.opComp _ _).inv := by cat_disch -set_option backward.defeqAttrib.useBackward true in /-- The "unopposite" of a natural transformation. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop where app X := (α.app (op X)).unop naturality X Y f := Quiver.Hom.op_inj (by simp) @@ -448,7 +429,6 @@ theorem unop_comp {F G H : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) : NatTrans.unop (α ≫ β) = NatTrans.unop β ≫ NatTrans.unop α := rfl -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma unop_whiskerRight {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H : Dᵒᵖ ⥤ Eᵒᵖ} (α : F ⟶ G) : NatTrans.unop (whiskerRight α H) = @@ -456,7 +436,6 @@ lemma unop_whiskerRight {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H (Functor.unopComp _ _).inv := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma unop_whiskerLeft {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H : Eᵒᵖ ⥤ Cᵒᵖ} (α : F ⟶ G) : NatTrans.unop (whiskerLeft H α) = @@ -467,7 +446,7 @@ lemma unop_whiskerLeft {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H /-- Given a natural transformation `α : F.op ⟶ G.op`, we can take the "unopposite" of each component obtaining a natural transformation `G ⟶ F`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def removeOp (α : F.op ⟶ G.op) : G ⟶ F where app X := (α.app (op X)).unop naturality X Y f := @@ -479,7 +458,7 @@ theorem removeOp_id (F : C ⥤ D) : NatTrans.removeOp (𝟙 F.op) = 𝟙 F := /-- Given a natural transformation `α : F.unop ⟶ G.unop`, we can take the opposite of each component obtaining a natural transformation `G ⟶ F`. -/ -@[simps, to_dual self] +@[implicit_reducible, simps, to_dual self] protected def removeUnop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) : G ⟶ F where app X := (α.app (unop X)).op naturality X Y f := @@ -495,11 +474,10 @@ section variable {F G H : C ⥤ Dᵒᵖ} -set_option backward.defeqAttrib.useBackward true in /-- Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`, taking `unop` of each component gives a natural transformation `G.leftOp ⟶ F.leftOp`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def leftOp (α : F ⟶ G) : G.leftOp ⟶ F.leftOp where app X := (α.app (unop X)).unop naturality X Y f := Quiver.Hom.op_inj (by simp) @@ -513,7 +491,6 @@ theorem leftOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.leftOp (α ≫ β) NatTrans.leftOp β ≫ NatTrans.leftOp α := rfl -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma leftOpWhiskerRight {E : Type*} [Category* E] {H : E ⥤ C} (α : F ⟶ G) : (whiskerLeft H α).leftOp = (Functor.leftOpComp H G).hom ≫ whiskerLeft _ α.leftOp ≫ @@ -523,7 +500,7 @@ lemma leftOpWhiskerRight {E : Type*} [Category* E] {H : E ⥤ C} (α : F ⟶ G) /-- Given a natural transformation `α : F.leftOp ⟶ G.leftOp`, for `F G : C ⥤ Dᵒᵖ`, taking `op` of each component gives a natural transformation `G ⟶ F`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def removeLeftOp (α : F.leftOp ⟶ G.leftOp) : G ⟶ F where app X := (α.app (op X)).op naturality X Y f := @@ -539,11 +516,10 @@ section variable {F G H : Cᵒᵖ ⥤ D} -set_option backward.defeqAttrib.useBackward true in /-- Given a natural transformation `α : F ⟶ G`, for `F G : Cᵒᵖ ⥤ D`, taking `op` of each component gives a natural transformation `G.rightOp ⟶ F.rightOp`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def rightOp (α : F ⟶ G) : G.rightOp ⟶ F.rightOp where app _ := (α.app _).op naturality X Y f := Quiver.Hom.unop_inj (by simp) @@ -557,7 +533,6 @@ theorem rightOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.rightOp (α ≫ β NatTrans.rightOp β ≫ NatTrans.rightOp α := rfl -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] lemma rightOpWhiskerRight {E : Type*} [Category* E] {H : D ⥤ E} (α : F ⟶ G) : (whiskerRight α H).rightOp = (Functor.rightOpComp G H).hom ≫ whiskerRight α.rightOp H.op ≫ @@ -567,7 +542,7 @@ lemma rightOpWhiskerRight {E : Type*} [Category* E] {H : D ⥤ E} (α : F ⟶ G) /-- Given a natural transformation `α : F.rightOp ⟶ G.rightOp`, for `F G : Cᵒᵖ ⥤ D`, taking `unop` of each component gives a natural transformation `G ⟶ F`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] protected def removeRightOp (α : F.rightOp ⟶ G.rightOp) : G ⟶ F where app X := (α.app X.unop).unop naturality X Y f := @@ -652,7 +627,6 @@ namespace NatIso variable {D : Type u₂} [Category.{v₂} D] variable {F G : C ⥤ D} -set_option backward.defeqAttrib.useBackward true in /-- The natural isomorphism between opposite functors `G.op ≅ F.op` induced by a natural isomorphism between the original functors `F ≅ G`. -/ @[simps] @@ -673,7 +647,6 @@ theorem op_trans {H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) : @[simp] theorem op_symm (α : F ≅ G) : NatIso.op α.symm = (NatIso.op α).symm := rfl -set_option backward.isDefEq.respectTransparency false in /-- The natural isomorphism between functors `G ≅ F` induced by a natural isomorphism between the opposite functors `F.op ≅ G.op`. -/ @[simps] @@ -681,7 +654,6 @@ protected def removeOp (α : F.op ≅ G.op) : G ≅ F where hom := NatTrans.removeOp α.hom inv := NatTrans.removeOp α.inv -set_option backward.defeqAttrib.useBackward true in /-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism between the original functors `F ≅ G`. -/ @[simps] @@ -700,33 +672,28 @@ theorem unop_trans {F G H : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) (β : G ≅ H) : @[simp] theorem unop_symm {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : NatIso.unop α.symm = (NatIso.unop α).symm := rfl -set_option backward.defeqAttrib.useBackward true in lemma op_isoWhiskerRight {E : Type*} [Category* E] {H : D ⥤ E} (α : F ≅ G) : NatIso.op (isoWhiskerRight α H) = (Functor.opComp _ _) ≪≫ isoWhiskerRight (NatIso.op α) H.op ≪≫ (Functor.opComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma op_isoWhiskerLeft {E : Type*} [Category* E] {H : E ⥤ C} (α : F ≅ G) : NatIso.op (isoWhiskerLeft H α) = (Functor.opComp _ _) ≪≫ isoWhiskerLeft H.op (NatIso.op α) ≪≫ (Functor.opComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma unop_whiskerRight {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H : Dᵒᵖ ⥤ Eᵒᵖ} (α : F ≅ G) : NatIso.unop (isoWhiskerRight α H) = (Functor.unopComp _ _) ≪≫ isoWhiskerRight (NatIso.unop α) H.unop ≪≫ (Functor.unopComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma unop_whiskerLeft {F G : Cᵒᵖ ⥤ Dᵒᵖ} {E : Type*} [Category* E] {H : Eᵒᵖ ⥤ Cᵒᵖ} (α : F ≅ G) : NatIso.unop (isoWhiskerLeft H α) = (Functor.unopComp _ _) ≪≫ isoWhiskerLeft H.unop (NatIso.unop α) ≪≫ (Functor.unopComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma op_leftUnitor : NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ @@ -734,7 +701,6 @@ lemma op_leftUnitor : (Functor.opComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma op_rightUnitor : NatIso.op F.rightUnitor = F.op.rightUnitor.symm ≪≫ @@ -742,7 +708,6 @@ lemma op_rightUnitor : (Functor.opComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma op_associator {E E' : Type*} [Category* E] [Category* E'] {F : C ⥤ D} {G : D ⥤ E} {H : E ⥤ E'} : NatIso.op (Functor.associator F G H) = @@ -751,7 +716,6 @@ lemma op_associator {E E' : Type*} [Category* E] [Category* E'] isoWhiskerRight (Functor.opComp _ _).symm H.op ≪≫ (Functor.opComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma unop_leftUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} : NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ @@ -759,7 +723,6 @@ lemma unop_leftUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} : (Functor.unopComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma unop_rightUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} : NatIso.unop F.rightUnitor = F.unop.rightUnitor.symm ≪≫ @@ -767,7 +730,6 @@ lemma unop_rightUnitor {F : Cᵒᵖ ⥤ Dᵒᵖ} : (Functor.unopComp _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in lemma unop_associator {E E' : Type*} [Category* E] [Category* E'] {F : Cᵒᵖ ⥤ Dᵒᵖ} {G : Dᵒᵖ ⥤ Eᵒᵖ} {H : Eᵒᵖ ⥤ E'ᵒᵖ} : NatIso.unop (Functor.associator F G H) = @@ -797,7 +759,6 @@ namespace Equivalence variable {D : Type u₂} [Category.{v₂} D] -set_option backward.defeqAttrib.useBackward true in /-- An equivalence between categories gives an equivalence between the opposite categories. -/ @[simps] @@ -810,7 +771,6 @@ def op (e : C ≌ D) : Cᵒᵖ ≌ Dᵒᵖ where apply Quiver.Hom.unop_inj simp -set_option backward.defeqAttrib.useBackward true in /-- An equivalence between opposite categories gives an equivalence between the original categories. -/ @[simps] @@ -823,15 +783,9 @@ def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D where apply Quiver.Hom.op_inj simp -#adaptation_note -/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in /-- An equivalence between `C` and `Dᵒᵖ` gives an equivalence between `Cᵒᵖ` and `D`. -/ @[simps!] def leftOp (e : C ≌ Dᵒᵖ) : Cᵒᵖ ≌ D := e.op.trans (opOpEquivalence D) -#adaptation_note -/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ -set_option backward.isDefEq.respectTransparency.types false in /-- An equivalence between `Cᵒᵖ` and `D` gives an equivalence between `C` and `Dᵒᵖ`. -/ @[simps!] def rightOp (e : Cᵒᵖ ≌ D) : C ≌ Dᵒᵖ := (opOpEquivalence C).symm.trans e.op @@ -881,7 +835,6 @@ namespace Functor variable (C) variable (D : Type u₂) [Category.{v₂} D] -set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in /-- The equivalence of functor categories induced by `op` and `unop`. -/ diff --git a/Mathlib/CategoryTheory/Whiskering.lean b/Mathlib/CategoryTheory/Whiskering.lean index 2398d24cc69..bece8bde3f5 100644 --- a/Mathlib/CategoryTheory/Whiskering.lean +++ b/Mathlib/CategoryTheory/Whiskering.lean @@ -42,27 +42,25 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] [Category.{v₃} E] /-- If `α : G ⟶ H` then `whiskerLeft F α : F ⋙ G ⟶ F ⋙ H` has components `α.app (F.obj X)`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] def whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : F ⋙ G ⟶ F ⋙ H where app X := α.app (F.obj X) naturality X Y f := by rw [Functor.comp_map, Functor.comp_map, α.naturality] -set_option backward.defeqAttrib.useBackward true in @[simp, to_dual self] lemma id_hcomp (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : 𝟙 F ◫ α = whiskerLeft F α := by ext simp /-- If `α : G ⟶ H` then `whiskerRight α F : G ⋙ F ⟶ H ⋙ F` has components `F.map (α.app X)`. -/ -@[to_dual self, simps (attr := to_dual self)] +@[implicit_reducible, to_dual self, simps (attr := to_dual self)] def whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : G ⋙ F ⟶ H ⋙ F where app X := F.map (α.app X) naturality X Y f := by rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality] -set_option backward.defeqAttrib.useBackward true in @[simp, to_dual self] lemma hcomp_id {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : α ◫ 𝟙 F = whiskerRight α F := by ext @@ -112,7 +110,6 @@ instance faithful_whiskeringRight_obj {F : D ⥤ E} [F.Faithful] : ext X exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X -set_option backward.isDefEq.respectTransparency false in /-- If `F : D ⥤ E` is fully faithful, then so is `(whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E`. -/ @[simps] @@ -202,7 +199,6 @@ theorem whiskerRight_comp {G H K : C ⥤ D} (α : G ⟶ H) (β : H ⟶ K) (F : D whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F := ((whiskeringRight C D E).obj F).map_comp α β -set_option backward.defeqAttrib.useBackward true in @[to_dual none, reassoc] theorem whiskerLeft_comp_whiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) : whiskerLeft F β ≫ whiskerRight α K = whiskerRight α H ≫ whiskerLeft G β := by @@ -300,7 +296,6 @@ theorem isoWhiskerRight_trans {G H K : C ⥤ D} (α : G ≅ H) (β : H ≅ K) (F isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F := ((whiskeringRight C D E).obj F).mapIso_trans α β -set_option backward.defeqAttrib.useBackward true in @[reassoc] theorem isoWhiskerLeft_trans_isoWhiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ≅ G) (β : H ≅ K) : isoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ isoWhiskerLeft G β := by @@ -309,21 +304,18 @@ theorem isoWhiskerLeft_trans_isoWhiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α variable {B : Type u₄} [Category.{v₄} B] -set_option backward.defeqAttrib.useBackward true in @[simp, to_dual none] theorem whiskerLeft_twice (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) : whiskerLeft F (whiskerLeft G α) = (Functor.associator _ _ _).inv ≫ whiskerLeft (F ⋙ G) α ≫ (Functor.associator _ _ _).hom := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[simp, to_dual none] theorem whiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) : whiskerRight (whiskerRight α F) G = (Functor.associator _ _ _).hom ≫ whiskerRight α (F ⋙ G) ≫ (Functor.associator _ _ _).inv := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[to_dual none] theorem whiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) : whiskerRight (whiskerLeft F α) K = @@ -343,7 +335,6 @@ theorem isoWhiskerRight_twice {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : Functor.associator _ _ _ ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (Functor.associator _ _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[reassoc] theorem isoWhiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) : isoWhiskerRight (isoWhiskerLeft F α) K = @@ -351,7 +342,6 @@ theorem isoWhiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D (Functor.associator _ _ _).symm := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[reassoc] theorem isoWhiskerLeft_right (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) : isoWhiskerLeft F (isoWhiskerRight α K) = @@ -367,25 +357,21 @@ variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B] {C : Type u₃} [Category.{v₃} C] {D : Type u₄} [Category.{v₄} D] {E : Type u₅} [Category.{v₅} E] (F : A ⥤ B) (G : B ⥤ C) (H : C ⥤ D) (K : D ⥤ E) -set_option backward.defeqAttrib.useBackward true in @[reassoc] theorem triangleIso : associator F (𝟭 B) G ≪≫ isoWhiskerLeft F (leftUnitor G) = isoWhiskerRight (rightUnitor F) G := by cat_disch -set_option backward.defeqAttrib.useBackward true in @[reassoc] theorem pentagonIso : isoWhiskerRight (associator F G H) K ≪≫ associator F (G ⋙ H) K ≪≫ isoWhiskerLeft F (associator G H K) = associator (F ⋙ G) H K ≪≫ associator F G (H ⋙ K) := by cat_disch -set_option backward.defeqAttrib.useBackward true in theorem triangle : (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G := by cat_disch -set_option backward.defeqAttrib.useBackward true in theorem pentagon : whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom = @@ -394,8 +380,6 @@ theorem pentagon : variable {C₁ C₂ C₃ D₁ D₂ D₃ : Type*} [Category* C₁] [Category* C₂] [Category* C₃] [Category* D₁] [Category* D₂] [Category* D₃] (E : Type*) [Category* E] -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- The obvious functor `(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)`. -/ @[simps!, implicit_reducible] def whiskeringLeft₂ : @@ -410,52 +394,45 @@ def whiskeringLeft₂ : { app := fun F₂ ↦ whiskerLeft _ ((whiskeringLeft C₁ D₁ (C₂ ⥤ E)).map ψ) } /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps!] +@[implicit_reducible, simps!] def whiskeringLeft₃ObjObjObj (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) (F₃ : C₃ ⥤ D₃) : (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E := (whiskeringRight _ _ _).obj (((whiskeringLeft₂ E).obj F₂).obj F₃) ⋙ (whiskeringLeft C₁ D₁ _).obj F₁ -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps] +@[implicit_reducible, simps] def whiskeringLeft₃ObjObjMap (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) {F₃ F₃' : C₃ ⥤ D₃} (τ₃ : F₃ ⟶ F₃') : whiskeringLeft₃ObjObjObj E F₁ F₂ F₃ ⟶ whiskeringLeft₃ObjObjObj E F₁ F₂ F₃' where app F := whiskerLeft _ (whiskerLeft _ (((whiskeringLeft₂ E).obj F₂).map τ₃)) -set_option backward.isDefEq.respectTransparency false in variable (C₃ D₃) in /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps] +@[implicit_reducible, simps] def whiskeringLeft₃ObjObj (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) : (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) where obj F₃ := whiskeringLeft₃ObjObjObj E F₁ F₂ F₃ map τ₃ := whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃ -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in variable (C₃ D₃) in /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps] +@[implicit_reducible, simps] def whiskeringLeft₃ObjMap (F₁ : C₁ ⥤ D₁) {F₂ F₂' : C₂ ⥤ D₂} (τ₂ : F₂ ⟶ F₂') : whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ ⟶ whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂' where app F₃ := whiskerRight ((whiskeringRight _ _ _).map (((whiskeringLeft₂ E).map τ₂).app F₃)) _ variable (C₂ C₃ D₂ D₃) in /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps] +@[implicit_reducible, simps] def whiskeringLeft₃Obj (F₁ : C₁ ⥤ D₁) : (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) where obj F₂ := whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ map τ₂ := whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂ -set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in variable (C₂ C₃ D₂ D₃) in /-- Auxiliary definition for `whiskeringLeft₃`. -/ -@[simps] +@[implicit_reducible, simps] def whiskeringLeft₃Map {F₁ F₁' : C₁ ⥤ D₁} (τ₁ : F₁ ⟶ F₁') : whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁ ⟶ whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁' where app F₂ := { app F₃ := whiskerLeft _ ((whiskeringLeft _ _ _).map τ₁) } From ca6d69cc839e29503761f6c9b60c6b1a0bb3cc91 Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Fri, 31 Jul 2026 08:53:46 +0000 Subject: [PATCH 02/14] feat(Algebra/QuadraticAlgebra): add the trace (#42207) Add `QuadraticAlgebra.trace`, the trace of a quadratic algebra as an `R`-linear map. (Also fixes two typos in docstrings.) --- Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 76 ++++++++++++++++++++- 1 file changed, 73 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean index 659edf8b374..d4c878ac16f 100644 --- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean +++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean @@ -11,7 +11,7 @@ public import Mathlib.Algebra.Star.Unitary import Mathlib.Tactic.FieldSimp /-! -# Quadratic algebras: involution and norm. +# Quadratic algebras: involution, norm, and trace. Let `R` be a commutative ring. We define: @@ -19,12 +19,14 @@ Let `R` be a commutative ring. We define: * `QuadraticAlgebra.norm`: the norm +* `QuadraticAlgebra.trace`: the trace, as an `R`-linear map + We prove: * `QuadraticAlgebra.isUnit_iff_norm_isUnit`: `w : QuadraticAlgebra R a b` is a unit iff `w.norm` is a unit in `R`. -* `QuadraticAlgebra.norm_mem_nonZero_divisors_iff`: +* `QuadraticAlgebra.norm_mem_nonZeroDivisors_iff`: `w : QuadraticAlgebra R a b` isn't a zero divisor iff `w.norm` isn't a zero divisor in `R`. @@ -148,7 +150,7 @@ section star variable [CommRing R] /-- Conjugation in `QuadraticAlgebra R a b`. -The conjugate of `x + y ω` is `x + y ω' = (x - a * y) - y ω`. -/ +The conjugate of `x + y ω` is `x + y ω' = (x + b * y) - y ω`. -/ instance : Star (QuadraticAlgebra R a b) where star z := ⟨z.re + b * z.im, -z.im⟩ @@ -180,6 +182,11 @@ instance : StarRing (QuadraticAlgebra R a b) where simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg] <;> ring star_add _ _ := QuadraticAlgebra.ext (by simp only [re_star, re_add, im_add]; ring) (neg_add _ _) +/-- `z - star z` is a multiple of the difference `ω - star ω`. -/ +theorem sub_star (z : QuadraticAlgebra R a b) : + z - star z = z.im • (ω - star ω) := by + ext <;> simp <;> ring + end star section norm @@ -302,6 +309,69 @@ theorem norm_mem_nonZeroDivisors_iff {z : QuadraticAlgebra R a b} : end norm +section trace + +variable [CommRing R] + +attribute [local grind =] re_add im_add im_star re_star re_smul im_smul RingHom.id_apply + algebraMap_re algebraMap_im + +/-- The trace in a quadratic algebra, as an `R`-linear map. -/ +def trace : QuadraticAlgebra R a b →ₗ[R] R where + toFun z := 2 * z.re + b * z.im + map_add' := by grind + map_smul' := by grind [smul_eq_mul] + +variable (z : QuadraticAlgebra R a b) + +theorem trace_def : trace z = 2 * z.re + b * z.im := rfl + +@[simp] +theorem trace_algebraMap (r : R) : + trace (algebraMap R (QuadraticAlgebra R a b) r) = 2 * r := by + grind [trace_def] + +@[simp] +theorem trace_natCast (n : ℕ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by + simp [trace_def, re_natCast, im_natCast] + +@[simp] +theorem trace_intCast (n : ℤ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by + simp [trace_def, re_intCast, im_intCast] + +@[simp] +theorem trace_omega : trace (ω : QuadraticAlgebra R a b) = b := by + simp [trace_def] + +@[simp] +theorem trace_one : trace (1 : QuadraticAlgebra R a b) = 2 := by + simp [trace_def] + +@[simp] +theorem trace_star : trace (star z) = trace z := by + grind [trace_def] + +/-- `z + star z` is the trace of `z`. -/ +theorem algebraMap_trace_eq_add_star : + algebraMap R (QuadraticAlgebra R a b) (trace z) = z + star z := by + ext <;> grind [trace_def] + +/-- The conjugate of `z` is `trace z - z`. -/ +theorem star_eq : + star z = algebraMap R (QuadraticAlgebra R a b) (trace z) - z := by + rw [algebraMap_trace_eq_add_star, add_sub_cancel_left] + +/-- Every element of a quadratic algebra satisfies its characteristic equation. -/ +theorem sq_sub_trace_smul_add_norm_eq_zero : + z ^ 2 - trace z • z + algebraMap R _ (norm z) = 0 := by + rw [Algebra.smul_def, algebraMap_trace_eq_add_star, algebraMap_norm_eq_mul_star]; ring + +theorem sq_eq_trace_smul_sub_norm : + z ^ 2 = trace z • z - algebraMap R _ (norm z) := by + rw [← sub_eq_zero, ← sub_add, sq_sub_trace_smul_add_norm_eq_zero] + +end trace + section field variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)] From d1906c820ac33cb410531db7a6277980309262db Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Fri, 31 Jul 2026 09:32:19 +0000 Subject: [PATCH 03/14] chore(Translate/ToDual): remove redundant entry from `abbreviationDict` (#42251) This PR removes the `setOfSucc` -> `setOfPred` translation from the `to_dual` abbreviation dictionary, since the `ofSucc` -> `ofPred` translation already implies it. --- Mathlib/Tactic/Translate/ToDual.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Translate/ToDual.lean b/Mathlib/Tactic/Translate/ToDual.lean index b1b34fed7d7..44bca9494aa 100644 --- a/Mathlib/Tactic/Translate/ToDual.lean +++ b/Mathlib/Tactic/Translate/ToDual.lean @@ -256,11 +256,10 @@ def abbreviationDict : Std.HashMap String String := .ofList [ ("leftOrdContinuous", "RightOrdContinuous"), ("rightOrdContinuous", "LeftOrdContinuous"), + -- Revert translations if they should not happen in certain word combinations: ("neTop", "NeBot"), ("decidableSucc", "DecidablePred"), - -- `Set.ofPred` is not dual to `Set.ofSucc` ("ofSucc", "OfPred"), - ("setOfSucc", "SetOfPred"), ] @[inherit_doc GuessName.GuessNameExt] From b2933a1c2279654385ef57ab547bc221f9b30365 Mon Sep 17 00:00:00 2001 From: Moritz Doll <21366319+mcdoll@users.noreply.github.com> Date: Fri, 31 Jul 2026 10:23:30 +0000 Subject: [PATCH 04/14] chore(Analysis/Seminorm): generalize typeclasses slightly (#42300) This is in preparation for disallowing `NormedSpace` in `Analysis.Seminorm`. --- Mathlib/Analysis/LocallyConvex/Basic.lean | 5 ++++- Mathlib/Analysis/Seminorm.lean | 4 ++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/LocallyConvex/Basic.lean b/Mathlib/Analysis/LocallyConvex/Basic.lean index 4ce40495bb0..98c9ae59a8f 100644 --- a/Mathlib/Analysis/LocallyConvex/Basic.lean +++ b/Mathlib/Analysis/LocallyConvex/Basic.lean @@ -6,7 +6,8 @@ Authors: Jean Lo, Bhavik Mehta, Yaël Dillies module public import Mathlib.Analysis.Convex.Hull -public import Mathlib.Analysis.Normed.Module.Basic +public import Mathlib.Analysis.Normed.Field.Lemmas +public import Mathlib.Analysis.Normed.MulAction public import Mathlib.Topology.Bornology.Absorbs /-! # Local convexity @@ -45,6 +46,8 @@ absorbent, balanced, locally convex, LCTVS @[expose] public section +assert_not_exists NormedSpace + open Set open scoped Pointwise Topology diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index b6cc241ca28..cdf425bd708 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -977,7 +977,7 @@ end NormedField section Convex -variable [NormedField 𝕜] [AddCommGroup E] [NormedSpace ℝ 𝕜] [Module 𝕜 E] +variable [NormedField 𝕜] [AddCommGroup E] [SMul ℝ 𝕜] [NormSMulClass ℝ 𝕜] [Module 𝕜 E] section SMul @@ -1018,7 +1018,7 @@ end Convex section RestrictScalars -variable (𝕜) {𝕜' : Type*} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] +variable (𝕜) {𝕜' : Type*} [NormedField 𝕜] [SeminormedRing 𝕜'] [SMul 𝕜 𝕜'] [NormSMulClass 𝕜 𝕜'] [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' E] /-- Reinterpret a seminorm over a field `𝕜'` as a seminorm over a smaller field `𝕜`. This will From 6ecc792a56a1f1287b2135eba94a3fb2ce2d01f7 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 31 Jul 2026 12:00:48 +0000 Subject: [PATCH 05/14] chore(GroupTheory): fix non-terminal simp (#42302) --- Mathlib/GroupTheory/SpecificGroups/Alternating.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean index 9a59091907c..2fe9015e1bc 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean @@ -318,7 +318,6 @@ theorem nontrivial_of_three_le_card (h3 : 3 ≤ Nat.card α) : Nontrivial (alter instance {n : ℕ} : Nontrivial (alternatingGroup (Fin (n + 3))) := nontrivial_of_three_le_card (by simp) -set_option linter.flexible false in -- TODO: fix non-terminal simp /-- Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation in $A_5$ is $A_5$. -/ @@ -332,9 +331,8 @@ theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alt rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h have h : Multiset.card g.cycleType ≤ 3 := le_of_mul_le_mul_right (le_trans h (by norm_num only [card_fin])) (by simp) - rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha - simp at ha - rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha + rw [mem_alternatingGroup, sign_of_cycleType, h2, Multiset.sum_replicate, Multiset.card_replicate, + smul_eq_mul, pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha swap; · decide rw [isConj_iff_cycleType_eq, h2] interval_cases h_1 : Multiset.card g.cycleType From 232b5fd2613910bc74c3f6372b0fb2b9ea677df8 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Fri, 31 Jul 2026 12:20:37 +0000 Subject: [PATCH 06/14] fix(Translate): support structures where a universe level doesn't appear in the type (#42228) This PR fixes a bug in `to_dual`/`to_additive` that makes it impossible to use it on a structure where a universe level doesn't appear in its type. --- Mathlib/Tactic/Translate/Core.lean | 11 ++++++++--- MathlibTest/Attribute/ToDual.lean | 8 ++++++++ 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean index f4696a0fa9b..a7e4bb221eb 100644 --- a/Mathlib/Tactic/Translate/Core.lean +++ b/Mathlib/Tactic/Translate/Core.lean @@ -1004,10 +1004,15 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config type{indentExpr tgtType}" -- Process any remaining universe contraints, to assign all universe metavariables. discard <| processPostponed (mayPostpone := false) (exceptionOnFailure := true) - let params ← levels.mapM fun level ↦ do match ← instantiateLevelMVars level with + let tgtParams := tgtDecl.levelParams.toArray + let params ← levels.mapIdxM fun i level ↦ do + match ← instantiateLevelMVars level with | .param u => return u - | _ => throwError "inferred universe `{level}` in `{srcType}` is not a parameter." - let some univReorder := getPermutation params.toArray tgtDecl.levelParams.toArray | + | _ => + -- For example in `HasLimitsOfSize`, not all universe levels appear in the type. + -- In that case, default to not permuting the universe levels. + return tgtParams[i]! + let some univReorder := getPermutation params.toArray tgtParams | throwError "inferred universe parameters {params} \ are not a reordering of {srcDecl.levelParams}." return ({ univReorder, reorder }, ← getRelevantArg t cfg relevantArg? src lint) diff --git a/MathlibTest/Attribute/ToDual.lean b/MathlibTest/Attribute/ToDual.lean index 539ba3e99d0..8b928456b9b 100644 --- a/MathlibTest/Attribute/ToDual.lean +++ b/MathlibTest/Attribute/ToDual.lean @@ -447,3 +447,11 @@ to_dual_name_hint Left Right, Epi Mono /-- info: "right_epi" -/ #guard_msgs in #eval return GuessName.guessName (data.guessNameExt.getState (← getEnv)) "left_mono" + +-- A structure with a universe not appearing in its type +structure HasLimitsOfSize where + foo : ∀ _ : Type u, True + +@[to_dual] +structure HasColimitsOfSize where + cofoo : ∀ _ : Type u, True From 45e3065c10669f3a91349ec140e6f218cfc162cd Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Fri, 31 Jul 2026 13:14:11 +0000 Subject: [PATCH 07/14] perf(AlgebraicGeometry/Group/Affine): specify the universe explicitly (#42303) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a universe annotation in `algΓAlgSpecAdjunction`, which was seemingly forgotten. This speeds it up by more that 10x. In the rest of the file, the universe is already specified everywhere. For an explanation of why a universe metavariable can cause such an enormous slowdown, see https://github.com/leanprover/lean4/issues/10414 --- Mathlib/AlgebraicGeometry/Group/Affine.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Group/Affine.lean b/Mathlib/AlgebraicGeometry/Group/Affine.lean index f35aa382472..8fc001b4a80 100644 --- a/Mathlib/AlgebraicGeometry/Group/Affine.lean +++ b/Mathlib/AlgebraicGeometry/Group/Affine.lean @@ -298,7 +298,7 @@ def Spec.mapMulEquiv {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Bi /-- The adjunction between `Spec` and `Γ` as functors between commutative `R`-algebras and schemes over `Spec R`. -/ -def algΓAlgSpecAdjunction (R : CommRingCat) : algΓ R ⊣ algSpec R := by +def algΓAlgSpecAdjunction (R : CommRingCat.{u}) : algΓ R ⊣ algSpec R := by have overAdjunction := Over.postAdjunctionRight (Y := .op <| R) ΓSpec.adjunction have overEquivAlg := ((Over.opEquivOpUnder R).trans (commAlgCatEquivUnder R).op.symm).toAdjunction simpa using! overAdjunction.comp overEquivAlg From 6a58949cc7b3db2cc8045f904fa21b9fc0954657 Mon Sep 17 00:00:00 2001 From: JX-Mo <296066944+JX-Mo@users.noreply.github.com> Date: Fri, 31 Jul 2026 13:35:12 +0000 Subject: [PATCH 08/14] feat(RepresentationTheory): add a surjectivity lemma for irreducible representations (#42151) Add a missing surjectivity lemma `surjective_or_eq_zero` for irreducible representations, parallel to the existing `injective_or_eq_zero` `bijective_or_eq_zero`. --- Mathlib/RepresentationTheory/Irreducible.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/RepresentationTheory/Irreducible.lean b/Mathlib/RepresentationTheory/Irreducible.lean index 85891bec9b6..df11ceb7d94 100644 --- a/Mathlib/RepresentationTheory/Irreducible.lean +++ b/Mathlib/RepresentationTheory/Irreducible.lean @@ -57,6 +57,10 @@ theorem injective_or_eq_zero : Injective f ∨ f = 0 := by rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)] exact LinearMap.injective_or_eq_zero (equivLinearMapAsModule ρ σ f) +theorem surjective_or_eq_zero (g : IntertwiningMap σ ρ) : Surjective g ∨ g = 0 := by + rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule σ ρ)] + exact LinearMap.surjective_or_eq_zero (equivLinearMapAsModule σ ρ g) + theorem bijective_or_eq_zero [IsIrreducible σ] : Bijective f ∨ f = 0 := by rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)] exact LinearMap.bijective_or_eq_zero (equivLinearMapAsModule ρ σ f) From a366f8766595f1297c03ef38b8d7ee326d75377a Mon Sep 17 00:00:00 2001 From: Fawad Haider <153737+FawadHa1der@users.noreply.github.com> Date: Fri, 31 Jul 2026 13:44:39 +0000 Subject: [PATCH 09/14] perf(MeasureTheory/Integral/IntervalIntegral/Periodic): explicit proof instead of aesop (#41870) The file speeds up by 25%, with significant impact on readability. --- .../MeasureTheory/Integral/IntervalIntegral/Periodic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean index 2a6fd7c4acb..cd33a5430f2 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean @@ -285,7 +285,7 @@ theorem intervalIntegrable {t : ℝ} (h₁f : Function.Periodic f T) wlog hT : 0 < T · rcases (not_lt.1 hT).eq_or_lt with h | h · tauto - · have hnT : 0 < -T := by aesop + · have hnT : 0 < -T := neg_pos.mpr h nth_rw 1 [(by ring : t = (t + T) + (-T))] at h₂f apply this h₁f.neg hnT.ne' h₂f.symm _ _ hnT -- Replace [a₁, a₂] by [t - n₁ * T, t + n₂ * T], where n₁ and n₂ are natural numbers @@ -307,7 +307,7 @@ theorem intervalIntegrable {t : ℝ} (h₁f : Function.Periodic f T) apply IntervalIntegrable.trans_iterate -- Show integrability over a shifted period intro k hk - convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) (by aesop)) using 1 + convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) enorm_ne_top) using 1 · funext x simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm · simp [a, Nat.cast_add] @@ -347,10 +347,10 @@ theorem intervalIntegral_add_eq (hf : Periodic f T) (t s : ℝ) : ∫ x in t..t + T, f x = ∫ x in s..s + T, f x := by wlog hT : 0 < T · rcases (not_lt.1 hT).eq_or_lt with hT | hT - · aesop + · simp [hT] · rw [← neg_inj, ← integral_symm, ← integral_symm] simpa only [← sub_eq_add_neg, add_sub_cancel_right] using - this hf.neg (t + T) (s + T) (by aesop : 0 < -T) + this hf.neg (t + T) (s + T) (neg_pos.mpr hT) simp only [integral_of_le, hT.le, le_add_iff_nonneg_right] have : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume := ⟨fun c s _ => measure_preimage_add _ _ _⟩ From ff4f94af10d0da3316c454c98b48cd7cb97f9ef7 Mon Sep 17 00:00:00 2001 From: Oliver Butterley <51876429+oliver-butterley@users.noreply.github.com> Date: Fri, 31 Jul 2026 13:44:42 +0000 Subject: [PATCH 10/14] feat (Linter/Header): add config for custom copyright (#41876) This PR adds the config option `linter.style.header.license` to the header linter. This allows downstream projects to use the linter on their projects even if they need to specify a different license or a different filename for the license. --- Mathlib/Tactic/Linter/Header.lean | 16 +++++++++++---- MathlibTest/Linter/Header/Basic.lean | 29 +++++++++++++++++++++++++++- 2 files changed, 40 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 40b79e7b281..cf0a0401129 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -175,11 +175,13 @@ The input is the copyright string, the output is an array of `Syntax × String` The linter checks that * the first and last line of the copyright are a `("/-", "-/")` pair, each on its own line; * the first line is begins with `Copyright (c) 20` and ends with `. All rights reserved.`; -* the second line is `Released under Apache 2.0 license as described in the file LICENSE.`; +* the second line equals `expectedLicense` (determined by the `linter.style.header.license` option, + defaults to the Mathlib default); * the remainder of the string begins with `Authors: `, does not end with `.` and contains no ` and ` nor a double space, except possibly after a line break. -/ -public def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) := Id.run do +public def copyrightHeaderChecks (copyright : String) (expectedLicense : String) : + Array (Syntax × String) := Id.run do -- First, we merge lines ending in `,`: two spaces after the line-break are ok, -- but so is only one or none. We take care of *not* adding more consecutive spaces, though. -- This is to allow the copyright or authors' lines to span several lines. @@ -240,7 +242,6 @@ public def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) "If an authors line spans multiple lines, \ each line but the last must end with a trailing comma") output := output.append (authorsLineChecks authorsLine authorsStart) - let expectedLicense := "Released under Apache 2.0 license as described in the file LICENSE." if license != expectedLicense then output := output.push (toSyntax copyright license, s!"Second copyright line should be \"{expectedLicense}\"") @@ -299,6 +300,12 @@ public register_option linter.style.header : Bool := { descr := "enable the header style linter" } +/-- The text required by `linter.style.header` as the second line of the header. -/ +public register_option linter.style.header.license : String := { + defValue := "Released under Apache 2.0 license as described in the file LICENSE." + descr := "The text required as the second line of the copyright header." +} + namespace Style.header /-- Check the `Syntax` `imports` for broad imports: @@ -437,7 +444,8 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do | _ => "" -- Report any errors about the copyright line. if mainModule != `Mathlib.Init && mainModule != `Mathlib.Tactic then - for (stx, m) in copyrightHeaderChecks copyright do + let expectedLicense := linter.style.header.license.get (← getOptions) + for (stx, m) in copyrightHeaderChecks copyright expectedLicense do Linter.logLint linter.style.header stx m!"* '{stx.getAtomVal}':\n{m}\n" -- Report a missing module doc-string. match afterImports with diff --git a/MathlibTest/Linter/Header/Basic.lean b/MathlibTest/Linter/Header/Basic.lean index 714f3240c91..1fb89a5e845 100644 --- a/MathlibTest/Linter/Header/Basic.lean +++ b/MathlibTest/Linter/Header/Basic.lean @@ -58,7 +58,8 @@ It logs details of what the linter would report if the `cop` is "malformed". elab "#check_copyright " copStx:str : command => do let cop := copStx.getString let offset := copStx.raw.getPos?.get!.increaseBy 1 - for (s, m) in Mathlib.Linter.copyrightHeaderChecks cop do + let expectedLicense := Mathlib.Linter.linter.style.header.license.get (← getOptions) + for (s, m) in Mathlib.Linter.copyrightHeaderChecks cop expectedLicense do if let some rg := s.getRange? then logInfoAt (.ofRange ({start := rg.start.offsetBy offset, stop := rg.stop.offsetBy offset})) m!"Text: `{replaceMultilineComments s.getAtomVal}`\n\ @@ -211,6 +212,32 @@ Authors: Name LastName -/ " +-- The required second line is configurable via the `linter.style.header.license` option. +/-- +info: Text: `Released under Apache 2.0 license as described in the file LICENSE.` +Range: (49, 116) +Message: 'Second copyright line should be "Released under the Custom License."' +-/ +#guard_msgs in +set_option linter.style.header.license "Released under the Custom License." in +#check_copyright +"/- +Copyright (c) 2026 Name. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Name +-/ +" + +-- A header whose second line matches the custom license is accepted. +set_option linter.style.header.license "Released under the Custom License." in +#check_copyright +"/- +Copyright (c) 2026 Name. All rights reserved. +Released under the Custom License. +Authors: Name +-/ +" + /-- info: Text: `A uthors:` Range: (126, 135) From d222514f99b0055e82a912e7e9e5cdb72e6abcfe Mon Sep 17 00:00:00 2001 From: ybenmeur <180416181+ybenmeur@users.noreply.github.com> Date: Fri, 31 Jul 2026 14:37:55 +0000 Subject: [PATCH 11/14] chore(FGModuleCat/EssentiallySmall): generalize to `Ring` (#42006) Replace the `CommRing` instance with `Ring`. --- Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean b/Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean index 5f569b9d613..e8aae510b9a 100644 --- a/Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean +++ b/Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean @@ -21,7 +21,7 @@ recommended to use the standard `CategoryTheory.SmallModel (FGModuleCat R)` inst universe v w u -variable (R : Type u) [CommRing R] +variable (R : Type u) [Ring R] open CategoryTheory From ce88332a27540b49d649b17a9d1a8c1cdfb9f193 Mon Sep 17 00:00:00 2001 From: Moritz Doll <21366319+mcdoll@users.noreply.github.com> Date: Fri, 31 Jul 2026 14:37:57 +0000 Subject: [PATCH 12/14] feat(LinearAlgebra): use `IsApply` for `QuadraticMap` (#42134) --- .../CliffordAlgebraNotInjective.lean | 4 +- .../CliffordAlgebra/Contraction.lean | 3 +- .../LinearAlgebra/CliffordAlgebra/Equivs.lean | 2 +- .../CliffordAlgebra/EvenEquiv.lean | 10 +- .../LinearAlgebra/QuadraticForm/Basic.lean | 117 ++++++------------ Mathlib/LinearAlgebra/QuadraticForm/Dual.lean | 8 +- 6 files changed, 51 insertions(+), 93 deletions(-) diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean index d06713dea37..391f689833d 100644 --- a/Counterexamples/CliffordAlgebraNotInjective.lean +++ b/Counterexamples/CliffordAlgebraNotInjective.lean @@ -163,10 +163,10 @@ def Q' : QuadraticForm K (Fin 3 → K) := ∑ i, sq i theorem Q'_add (x y : Fin 3 → K) : Q' (x + y) = Q' x + Q' y := by - simp only [Q', QuadraticMap.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib] + simp only [Q', sum_apply, sq_map_add_char_two, Finset.sum_add_distrib] theorem Q'_sub (x y : Fin 3 → K) : Q' (x - y) = Q' x - Q' y := by - simp only [Q', QuadraticMap.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib] + simp only [Q', sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib] theorem Q'_apply (a : Fin 3 → K) : Q' a = a 0 * a 0 + a 1 * a 1 + a 2 * a 2 := calc diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean index 75e22d61ca3..1cf62573ab4 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean @@ -242,8 +242,7 @@ def changeForm (h : B.toQuadraticMap = Q' - Q) : CliffordAlgebra Q →ₗ[R] Cli foldr Q (changeFormAux Q' B) (fun m x => (changeFormAux_changeFormAux Q' B m x).trans <| by - dsimp only [← BilinMap.toQuadraticMap_apply] - rw [h, QuadraticMap.sub_apply, sub_sub_cancel]) + rw [← BilinMap.toQuadraticMap_apply, h, sub_apply, sub_sub_cancel]) 1 /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/ diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index cc95bd4a21c..69383a1c5d0 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -341,7 +341,7 @@ variable {R : Type*} [CommRing R] theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul r₁, ← smul_eq_mul r₂, map_smul, map_smul, - smul_mul_smul_comm, ι_sq_scalar, QuadraticMap.zero_apply, map_zero, smul_zero] + smul_mul_smul_comm, ι_sq_scalar, zero_apply, map_zero, smul_zero] set_option backward.isDefEq.respectTransparency.types false in /-- The clifford algebra over a 1-dimensional vector space with 0 quadratic form is isomorphic to diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean index fc30d6145d9..5dbfba9992d 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean @@ -74,9 +74,7 @@ theorem v_sq_scalar (m : M) : v Q m * v Q m = algebraMap _ _ (Q m) := set_option backward.defeqAttrib.useBackward true in theorem neg_e0_mul_v (m : M) : -(e0 Q * v Q m) = v Q m * e0 Q := by refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_) - dsimp [QuadraticMap.polar] - simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, - add_sub_cancel_right, sub_self, map_zero] + simp [QuadraticMap.polar] theorem neg_v_mul_e0 (m : M) : -(v Q m * e0 Q) = e0 Q * v Q m := by rw [neg_eq_iff_eq_neg] @@ -228,10 +226,10 @@ def evenToNeg (Q' : QuadraticForm R M) (h : Q' = -Q) : even.lift Q <| { bilin := -(even.ι Q' :).bilin contract := fun m => by - simp_rw [LinearMap.neg_apply, EvenHom.contract, h, QuadraticMap.neg_apply, map_neg, neg_neg] + simp_rw [LinearMap.neg_apply, EvenHom.contract, h, neg_apply, map_neg, neg_neg] contract_mid := fun m₁ m₂ m₃ => by - simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h, - QuadraticMap.neg_apply, smul_neg, neg_smul] } + simp_rw [LinearMap.neg_apply, neg_mul_neg, EvenHom.contract_mid, h, neg_apply, smul_neg, + neg_smul] } @[simp] theorem evenToNeg_ι (Q' : QuadraticForm R M) (h : Q' = -Q) (m₁ m₂ : M) : diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index ecbafd2a2f8..a89e55fcc8c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -408,19 +408,18 @@ instance : SMul S (QuadraticMap R M N) := letI := SMulCommClass.symm S R N ⟨a • B, by simp [h]⟩ }⟩ -@[simp, norm_cast] -theorem coeFn_smul (a : S) (Q : QuadraticMap R M N) : ⇑(a • Q) = a • ⇑Q := - rfl +instance : IsSMulApply S (QuadraticMap R M N) M N where + smul_apply _ _ _ := rfl -@[simp] -theorem smul_apply (a : S) (Q : QuadraticMap R M N) (x : M) : (a • Q) x = a • Q x := - rfl +@[deprecated (since := "2026-07-27")] alias coeFn_smul := FunLike.coe_smul + +@[deprecated (since := "2026-07-27")] protected alias smul_apply := smul_apply -instance [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M N) where - smul_comm _s _t _q := ext fun _ => smul_comm _ _ _ +instance [SMulCommClass S T N] : SMulCommClass S T (QuadraticMap R M N) := + FunLike.smulCommClass -instance [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N) where - smul_assoc _s _t _q := ext fun _ => smul_assoc _ _ _ +instance [SMul S T] [IsScalarTower S T N] : IsScalarTower S T (QuadraticMap R M N) := + FunLike.isScalarTower end SMul @@ -429,13 +428,12 @@ instance : Zero (QuadraticMap R M N) := toFun_smul := fun a _ => by simp only [smul_zero] exists_companion' := ⟨0, fun _ _ => by simp only [add_zero, LinearMap.zero_apply]⟩ }⟩ -@[simp, norm_cast] -theorem coeFn_zero : ⇑(0 : QuadraticMap R M N) = 0 := - rfl +instance : IsZeroApply (QuadraticMap R M N) M N where + zero_apply _ := rfl -@[simp] -theorem zero_apply (x : M) : (0 : QuadraticMap R M N) x = 0 := - rfl +@[deprecated (since := "2026-07-27")] alias coeFn_zero := FunLike.coe_zero + +@[deprecated (since := "2026-07-27")] protected alias zero_apply := zero_apply instance : Inhabited (QuadraticMap R M N) := ⟨0⟩ @@ -450,64 +448,33 @@ instance : Add (QuadraticMap R M N) := ⟨B + B', fun x y => by simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_comm]⟩ }⟩ -@[simp, norm_cast] -theorem coeFn_add (Q Q' : QuadraticMap R M N) : ⇑(Q + Q') = Q + Q' := - rfl +instance : IsAddApply (QuadraticMap R M N) M N where + add_apply _ _ _ := rfl -@[simp] -theorem add_apply (Q Q' : QuadraticMap R M N) (x : M) : (Q + Q') x = Q x + Q' x := - rfl +@[deprecated (since := "2026-07-27")] alias coeFn_add := FunLike.coe_add -instance : AddCommMonoid (QuadraticMap R M N) := - DFunLike.coe_injective.addCommMonoid _ coeFn_zero coeFn_add fun _ _ => coeFn_smul _ _ +@[deprecated (since := "2026-07-27")] protected alias add_apply := add_apply -/-- `@CoeFn (QuadraticMap R M)` as an `AddMonoidHom`. +instance : AddCommMonoid (QuadraticMap R M N) := fast_instance% FunLike.addCommMonoid -This API mirrors `AddMonoidHom.coeFn`. -/ -@[simps apply] -def coeFnAddMonoidHom : QuadraticMap R M N →+ M → N where - toFun := DFunLike.coe - map_zero' := coeFn_zero - map_add' := coeFn_add +@[deprecated (since := "2026-07-27")] alias coeFnAddMonoidHom := FunLike.coeAddMonoidHom + +@[deprecated (since := "2026-07-27")] alias coeFnAddMonoidHom_apply := FunLike.coeAddMonoidHom_apply /-- Evaluation on a particular element of the module `M` is an additive map on quadratic maps. -/ @[simps! apply] def evalAddMonoidHom (m : M) : QuadraticMap R M N →+ N := - (Pi.evalAddMonoidHom _ m).comp coeFnAddMonoidHom + (Pi.evalAddMonoidHom _ m).comp (FunLike.coeAddMonoidHom _ _ _) -section Sum +@[deprecated (since := "2026-07-27")] alias coeFn_sum := FunLike.coe_sum -@[simp, norm_cast] -theorem coeFn_sum {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) : - ⇑(∑ i ∈ s, Q i) = ∑ i ∈ s, ⇑(Q i) := - map_sum coeFnAddMonoidHom Q s - -@[simp] -theorem sum_apply {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) (x : M) : - (∑ i ∈ s, Q i) x = ∑ i ∈ s, Q i x := - map_sum (evalAddMonoidHom x : _ →+ N) Q s - -end Sum +@[deprecated (since := "2026-07-27")] protected alias sum_apply := sum_apply instance [Monoid S] [DistribMulAction S N] [SMulCommClass S R N] : - DistribMulAction S (QuadraticMap R M N) where - mul_smul a b Q := ext fun x => by simp only [smul_apply, mul_smul] - one_smul Q := ext fun x => by simp only [QuadraticMap.smul_apply, one_smul] - smul_add a Q Q' := by - ext - simp only [add_apply, smul_apply, smul_add] - smul_zero a := by - ext - simp only [zero_apply, smul_apply, smul_zero] + DistribMulAction S (QuadraticMap R M N) := fast_instance% FunLike.distribMulAction instance [Semiring S] [Module S N] [SMulCommClass S R N] : - Module S (QuadraticMap R M N) where - zero_smul Q := by - ext - simp only [zero_apply, smul_apply, zero_smul] - add_smul a b Q := by - ext - simp only [add_apply, smul_apply, add_smul] + Module S (QuadraticMap R M N) := fast_instance% FunLike.module end SemiringOperators @@ -523,28 +490,24 @@ instance : Neg (QuadraticMap R M N) := let ⟨B, h⟩ := Q.exists_companion ⟨-B, fun x y => by simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]⟩ }⟩ -@[simp, norm_cast] -theorem coeFn_neg (Q : QuadraticMap R M N) : ⇑(-Q) = -Q := - rfl +instance : IsNegApply (QuadraticMap R M N) M N where + neg_apply _ _ := rfl -@[simp] -theorem neg_apply (Q : QuadraticMap R M N) (x : M) : (-Q) x = -Q x := - rfl +@[deprecated (since := "2026-07-27")] alias coeFn_neg := FunLike.coe_neg + +@[deprecated (since := "2026-07-27")] protected alias neg_apply := neg_apply instance : Sub (QuadraticMap R M N) := ⟨fun Q Q' => (Q + -Q').copy (Q - Q') (sub_eq_add_neg _ _)⟩ -@[simp, norm_cast] -theorem coeFn_sub (Q Q' : QuadraticMap R M N) : ⇑(Q - Q') = Q - Q' := - rfl +instance : IsSubApply (QuadraticMap R M N) M N where + sub_apply _ _ _ := rfl -@[simp] -theorem sub_apply (Q Q' : QuadraticMap R M N) (x : M) : (Q - Q') x = Q x - Q' x := - rfl +@[deprecated (since := "2026-07-27")] alias coeFn_sub := FunLike.coe_sub -instance : AddCommGroup (QuadraticMap R M N) := - DFunLike.coe_injective.addCommGroup _ coeFn_zero coeFn_add coeFn_neg coeFn_sub - (fun _ _ => coeFn_smul _ _) fun _ _ => coeFn_smul _ _ +@[deprecated (since := "2026-07-27")] protected alias sub_apply := sub_apply + +instance : AddCommGroup (QuadraticMap R M N) := fast_instance% FunLike.addCommGroup end RingOperators @@ -573,7 +536,6 @@ section Comp variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] variable [AddCommMonoid P] [Module R P] -set_option backward.isDefEq.respectTransparency false in /-- Compose the quadratic map with a linear function on the right. -/ def comp (Q : QuadraticMap R N P) (f : M →ₗ[R] N) : QuadraticMap R M P where toFun x := Q (f x) @@ -586,7 +548,6 @@ def comp (Q : QuadraticMap R N P) (f : M →ₗ[R] N) : QuadraticMap R M P where theorem comp_apply (Q : QuadraticMap R N P) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x) := rfl -set_option backward.isDefEq.respectTransparency false in /-- Compose a quadratic map with a linear function on the left. -/ @[simps +simpRhs] def _root_.LinearMap.compQuadraticMap (f : N →ₗ[R] P) (Q : QuadraticMap R M N) : @@ -1465,7 +1426,7 @@ end theorem weightedSumSquares_apply [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (v : ι → R) : weightedSumSquares R w v = ∑ i : ι, w i • (v i * v i) := - QuadraticMap.sum_apply _ _ _ + sum_apply _ _ _ /-- On an orthogonal basis, the basis representation of `Q` is just a sum of squares. -/ theorem basisRepr_eq_of_iIsOrtho {R M} [CommRing R] [AddCommGroup M] [Module R M] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean index fe0a872ae49..0f63ac84e22 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean @@ -141,10 +141,10 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply, - LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, QuadraticMap.prod_apply, - QuadraticMap.neg_apply] - simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2, - smul_sub, Module.End.smul_def, sub_add_sub_cancel, ← sub_eq_add_neg (Q x.1) (Q x.2)] + LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, QuadraticMap.prod_apply] + simp only [neg_apply, polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, + polar_comm _ x.1 x.2, smul_sub, Module.End.smul_def, sub_add_sub_cancel, + ← sub_eq_add_neg (Q x.1) (Q x.2)] rw [← map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def] simp only [Module.End.smul_def, half_moduleEnd_apply_eq_half_smul, smul_eq_mul, invOf_mul_cancel_left'] From f4570dc2f3c801ed0c0edd5867f943e2b84e4dec Mon Sep 17 00:00:00 2001 From: Thomas Browning <13339017+tb65536@users.noreply.github.com> Date: Fri, 31 Jul 2026 17:06:37 +0000 Subject: [PATCH 13/14] chore(RingTheory/*): remove domain assumptions by generalizing from torsion free to faithful smul (#41379) This PR removes some `IsDomain` assumptions by generalizing `Module.IsTorsionFree` to `FaithfulSMul`. (As @SnirBroshi pointed out in the comments, this is not quite a generalization when the top ring is the zero ring, but this never arises in practice). Co-authored-by: tb65536 --- Mathlib/RingTheory/Conductor.lean | 4 +--- Mathlib/RingTheory/Ideal/Maps.lean | 4 ++-- Mathlib/RingTheory/Ideal/Over.lean | 11 ++++++----- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Mathlib/RingTheory/Conductor.lean b/Mathlib/RingTheory/Conductor.lean index e858142535f..01c6d097802 100644 --- a/Mathlib/RingTheory/Conductor.lean +++ b/Mathlib/RingTheory/Conductor.lean @@ -63,11 +63,9 @@ theorem conductor_eq_top_iff_adjoin_eq_top {x : S} : open IsLocalization in lemma mem_coeSubmodule_conductor {L} [CommRing L] [Algebra S L] [Algebra R L] - [IsScalarTower R S L] [IsDomain S] [IsTorsionFree S L] {x : S} {y : L} : + [IsScalarTower R S L] [FaithfulSMul S L] {x : S} {y : L} : y ∈ coeSubmodule L (conductor R x) ↔ ∀ z : S, y * (algebraMap S L) z ∈ R[algebraMap S L x] := by - cases subsingleton_or_nontrivial L - · rw [Subsingleton.elim (coeSubmodule L _) ⊤, Subsingleton.elim (Algebra.adjoin R _) ⊤]; simp trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L) · simp only [coeSubmodule, Submodule.mem_map, linearMap_apply, Subalgebra.mem_map, IsScalarTower.coe_toAlgHom'] diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 042bd37972f..2dd5b251324 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -1128,8 +1128,8 @@ section CommRing variable [CommRing R] [CommRing S] -theorem map_ne_bot_of_ne_bot [IsDomain R] {S : Type*} [Ring S] [Nontrivial S] [Algebra R S] - [Module.IsTorsionFree R S] {I : Ideal R} (h : I ≠ ⊥) : map (algebraMap R S) I ≠ ⊥ := +theorem map_ne_bot_of_ne_bot {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S] + [FaithfulSMul R S] {I : Ideal R} (h : I ≠ ⊥) : map (algebraMap R S) I ≠ ⊥ := (map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)).mp.mt h theorem map_eq_iff_sup_ker_eq_of_surjective {I J : Ideal R} (f : R →+* S) diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index cc305ab486e..00575891528 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/Mathlib/RingTheory/Ideal/Over.lean @@ -256,8 +256,8 @@ end CommSemiring section CommRing -variable (A B : Type*) [CommRing A] [IsDomain A] [Ring B] [Nontrivial B] - [Algebra A B] [Module.IsTorsionFree A B] {p : Ideal A} +variable (A B : Type*) [CommSemiring A] [Semiring B] + [Algebra A B] [FaithfulSMul A B] {p : Ideal A} @[simp] theorem under_bot : under A (⊥ : Ideal B) = ⊥ := @@ -389,9 +389,10 @@ abbrev primesOver.mk (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] : prime ⟨P, ⟨hPp, hp⟩⟩ variable {p} in -theorem ne_bot_of_mem_primesOver [IsDomain R] {S : Type*} [Ring S] [Algebra R S] [Nontrivial S] - [Module.IsTorsionFree R S] {p : Ideal R} (hp : p ≠ ⊥) {P : Ideal S} (hP : P ∈ p.primesOver S) : - P ≠ ⊥ := by have : P.LiesOver p := hP.2; exact ne_bot_of_liesOver_of_ne_bot hp P +theorem ne_bot_of_mem_primesOver [FaithfulSMul A B] (hp : p ≠ ⊥) {P : Ideal B} + (hP : P ∈ p.primesOver B) : P ≠ ⊥ := by + have : P.LiesOver p := hP.2 + exact ne_bot_of_liesOver_of_ne_bot hp P end primesOver From 1f8806b67d6f09e6d2552c031e6d3a3171016116 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Fri, 31 Jul 2026 22:26:39 +0000 Subject: [PATCH 14/14] fix: adaptations for batteries #1927 (#42229) After [batteries#1927](https://github.com/leanprover-community/batteries/pull/1927) is merged: - [x] Merge leanprover-community/mathlib4:master - [x] Edit the lakefile to point to leanprover-community/batteries:main - [x] Run lake update batteries - [ ] Wait for CI and merge Co-authored-by: mathlib-nightly-testing[bot] --- Mathlib/Data/Fintype/Perm.lean | 3 ++- Mathlib/Data/List/Destutter.lean | 3 ++- Mathlib/Data/List/Lookmap.lean | 6 +++--- Mathlib/Data/List/Sublists.lean | 2 +- Mathlib/GroupTheory/Perm/ClosureSwap.lean | 8 ++++---- Mathlib/GroupTheory/Perm/List.lean | 18 +++++++++--------- lake-manifest.json | 2 +- 7 files changed, 22 insertions(+), 20 deletions(-) diff --git a/Mathlib/Data/Fintype/Perm.lean b/Mathlib/Data/Fintype/Perm.lean index 49f2a6858af..eba49a68098 100644 --- a/Mathlib/Data/Fintype/Perm.lean +++ b/Mathlib/Data/Fintype/Perm.lean @@ -64,7 +64,8 @@ theorem mem_permsOfList_of_mem {l : List α} {f : Perm α} (h : ∀ x, f x ≠ x simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap] refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩ · exact mem_of_ne_of_mem hfa (h _ hfa') - · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul] + · rw [← mul_assoc, mul_def (Equiv.swap a (f a)) (Equiv.swap a (f a)), Equiv.swap_swap, + ← Perm.one_def, one_mul] theorem mem_of_mem_permsOfList : ∀ {l : List α} {f : Perm α}, f ∈ permsOfList l → {x : α} → f x ≠ x → x ∈ l diff --git a/Mathlib/Data/List/Destutter.lean b/Mathlib/Data/List/Destutter.lean index 389ba61aef5..17264eea64d 100644 --- a/Mathlib/Data/List/Destutter.lean +++ b/Mathlib/Data/List/Destutter.lean @@ -89,7 +89,8 @@ theorem isChain_destutter' (l : List α) (a : α) : (l.destutter' R a).IsChain R simp_rw [destutter'_cons, apply_ite (IsChain R ·), apply_ite (IsChain R <| a :: ·), IH, isChain_cons_cons, if_true_right, ite_prop_iff_and, imp_and] - exact ⟨⟨⟨swap <| fun _ => id, fun _ => IH2 c b⟩, swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩ + exact ⟨⟨⟨Function.swap <| fun _ => id, fun _ => IH2 c b⟩, + Function.swap <| fun _ => IH2 b a⟩, fun _ => IH2 c a⟩ theorem isChain_cons_destutter'_of_rel (l : List α) {a b} (hab : R a b) : (a :: l.destutter' R b).IsChain R := by diff --git a/Mathlib/Data/List/Lookmap.lean b/Mathlib/Data/List/Lookmap.lean index bf9569cdc72..6f230a97b1f 100644 --- a/Mathlib/Data/List/Lookmap.lean +++ b/Mathlib/Data/List/Lookmap.lean @@ -102,9 +102,9 @@ theorem perm_lookmap (f : α → Option α) {l₁ l₂ : List α} · simp [lookmap_cons_some _ _ h, p] | swap a b l => rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d - · simpa [h₁, h₂] using swap _ _ _ - · simpa [h₁, lookmap_cons_some _ _ h₂] using swap _ _ _ - · simpa [lookmap_cons_some _ _ h₁, h₂] using swap _ _ _ + · simpa [h₁, h₂] using Perm.swap _ _ _ + · simpa [h₁, lookmap_cons_some _ _ h₂] using Perm.swap _ _ _ + · simpa [lookmap_cons_some _ _ h₁, h₂] using Perm.swap _ _ _ · rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩ exact Perm.refl _ | trans p₁ _ IH₁ IH₂ => diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index e41e39c15a6..f7d84b06351 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/Mathlib/Data/List/Sublists.lean @@ -301,7 +301,7 @@ theorem sublistsLen_length : ∀ l : List α, sublistsLen l.length l = [l] open Function theorem Pairwise.sublists' {R} : - ∀ {l : List α}, Pairwise R l → Pairwise (Lex (swap R)) (sublists' l) + ∀ {l : List α}, Pairwise R l → Pairwise (Lex (Function.swap R)) (sublists' l) | _, Pairwise.nil => pairwise_singleton _ _ | _, @Pairwise.cons _ _ a l H₁ H₂ => by simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp, diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean index 7a8cb3d3f0d..333bcdfe2e2 100644 --- a/Mathlib/GroupTheory/Perm/ClosureSwap.lean +++ b/Mathlib/GroupTheory/Perm/ClosureSwap.lean @@ -75,7 +75,7 @@ theorem SubmonoidClass.swap_mem_trans {a b c : α} {C} [SetLike C (Perm α)] · exact hbc obtain rfl | hac := eq_or_ne a c · exact swap_self a ▸ one_mem M - rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac] + rw [Equiv.swap_comm, ← swap_mul_swap_mul_swap hab' hac] exact mul_mem (mul_mem hbc hab) hbc /-- If a subgroup is generated by transpositions, then a transposition `swap x y` lies in the @@ -91,10 +91,10 @@ theorem swap_mem_closure_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap) have := ne_of_mem_of_not_mem ha hσa rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha) - obtain rfl | rfl := this <;> simpa [swap_comm] using subset_closure hσ + obtain rfl | rfl := this <;> simpa [Equiv.swap_comm] using subset_closure hσ · obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv] · exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩ - · rw [mem_ofPred, swap_self]; apply one_mem + · rw [mem_ofPred, Equiv.swap_self]; apply one_mem /-- If a subgroup is generated by transpositions, then a permutation `f` lies in the subgroup if and only if `f` has finite support and `f x` always lies in the same orbit as `x`. -/ @@ -128,7 +128,7 @@ theorem mem_closure_isSwap' {f : Perm α} : refine (mem_closure_isSwap fun _ ↦ id).trans (and_iff_left fun x ↦ ⟨⟨swap x (f x), ?_⟩, swap_apply_left x (f x)⟩) by_cases h : x = f x - · rw [← h, swap_self] + · rw [← h, Equiv.swap_self] apply Subgroup.one_mem · exact subset_closure ⟨x, f x, h, rfl⟩ diff --git a/Mathlib/GroupTheory/Perm/List.lean b/Mathlib/GroupTheory/Perm/List.lean index 0fc68bae856..a0435100d48 100644 --- a/Mathlib/GroupTheory/Perm/List.lean +++ b/Mathlib/GroupTheory/Perm/List.lean @@ -60,31 +60,31 @@ theorem formPerm_singleton (x : α) : formPerm [x] = 1 := @[simp] theorem formPerm_cons_cons (x y : α) (l : List α) : - formPerm (x :: y :: l) = swap x y * formPerm (y :: l) := + formPerm (x :: y :: l) = Equiv.swap x y * formPerm (y :: l) := rfl -theorem formPerm_pair (x y : α) : formPerm [x, y] = swap x y := +theorem formPerm_pair (x y : α) : formPerm [x, y] = Equiv.swap x y := rfl theorem mem_or_mem_of_zipWith_swap_prod_ne : ∀ {l l' : List α} {x : α}, - (zipWith swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l' + (zipWith Equiv.swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l' | [], _, _ => by simp | _, [], _ => by simp | a::l, b::l', x => fun hx ↦ - if h : (zipWith swap l l').prod x = x then + if h : (zipWith Equiv.swap l l').prod x = x then (eq_or_eq_of_swap_apply_ne_self (a := a) (b := b) (x := x) (by simpa [h] using hx)).imp (by rintro rfl; exact .head _) (by rintro rfl; exact .head _) else (mem_or_mem_of_zipWith_swap_prod_ne h).imp (.tail _) (.tail _) theorem zipWith_swap_prod_support' (l l' : List α) : - { x | (zipWith swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := fun _ h ↦ by + { x | (zipWith Equiv.swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := fun _ h ↦ by simpa using mem_or_mem_of_zipWith_swap_prod_ne h theorem zipWith_swap_prod_support [Fintype α] (l l' : List α) : - (zipWith swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset := by + (zipWith Equiv.swap l l').prod.support ≤ l.toFinset ⊔ l'.toFinset := by intro x hx - have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx + have hx' : x ∈ { x | (zipWith Equiv.swap l l').prod x ≠ x } := by simpa using hx simpa using zipWith_swap_prod_support' _ _ hx' theorem support_formPerm_le' : { x | formPerm l x ≠ x } ≤ l.toFinset := by @@ -239,7 +239,7 @@ theorem formPerm_eq_of_isRotated {l l' : List α} (hd : Nodup l) (h : l ~r l') : exact (formPerm_rotate l hd n).symm theorem formPerm_append_pair : ∀ (l : List α) (a b : α), - formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b + formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * Equiv.swap a b | [], _, _ => rfl | [_], _, _ => rfl | x::y::l, a, b => by @@ -249,7 +249,7 @@ theorem formPerm_reverse : ∀ l : List α, formPerm l.reverse = (formPerm l)⁻ | [] => rfl | [_] => rfl | a::b::l => by - simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)] + simp [formPerm_append_pair, Equiv.swap_comm, ← formPerm_reverse (b::l)] theorem formPerm_pow_apply_getElem (l : List α) (w : Nodup l) (n : ℕ) (i : ℕ) (h : i < l.length) : (formPerm l ^ n) l[i] = diff --git a/lake-manifest.json b/lake-manifest.json index 43aaa30cab5..3ac6d313b04 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "41bd267b3f6b7252f6676af46d4ffc6783b64de9", + "rev": "ae82a25d0eb1259a7044d6b77adb21475ff13233", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",