Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

refactor: deprecate ContinuousMonoidHomClass #17558

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
+51 −52
Open

refactor: deprecate ContinuousMonoidHomClass #17558

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
22af102
refactor: deprecate `ContinuousMonoidHomClass`
urkud Oct 8, 2024
29a5790
Add missing docs
urkud Oct 8, 2024
62b1af9
Fix `mk'`
urkud Oct 9, 2024
764fb7b
Update
urkud Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
94 changes: 45 additions & 49 deletions Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,49 +30,45 @@ variable (F A B C D E : Type*) [Monoid A] [Monoid B] [Monoid C] [Monoid D] [Comm
/-- The type of continuous additive monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousAddMonoidHom A B)`,
you should parametrize over `(F : Type*) [ContinuousAddMonoidHomClass F A B] (f : F)`.
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F)`.

When you extend this structure, make sure to extend `ContinuousAddMonoidHomClass`. -/
When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `AddMonoidHomClass`, if needed. -/
structure ContinuousAddMonoidHom (A B : Type*) [AddMonoid A] [AddMonoid B] [TopologicalSpace A]
[TopologicalSpace B] extends A →+ B where
/-- Proof of continuity of the Hom. -/
continuous_toFun : @Continuous A B _ _ toFun
[TopologicalSpace B] extends A →+ B, C(A, B)

/-- The type of continuous monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousMonoidHom A B)`,
you should parametrize over `(F : Type*) [ContinuousMonoidHomClass F A B] (f : F)`.
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F)`.

When you extend this structure, make sure to extend `ContinuousAddMonoidHomClass`. -/
When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `MonoidHomClass`, if needed. -/
@[to_additive "The type of continuous additive monoid homomorphisms from `A` to `B`."]
structure ContinuousMonoidHom extends A →* B where
/-- Proof of continuity of the Hom. -/
continuous_toFun : @Continuous A B _ _ toFun
structure ContinuousMonoidHom extends A →* B, C(A, B)

section

/-- `ContinuousAddMonoidHomClass F A B` states that `F` is a type of continuous additive monoid
homomorphisms.

You should also extend this typeclass when you extend `ContinuousAddMonoidHom`. -/
-- Porting note: Changed A B to outParam to help synthesizing order
class ContinuousAddMonoidHomClass (A B : outParam Type*) [AddMonoid A] [AddMonoid B]
Deprecated and changed from a `class` to a `structure`.
Use `[AddMonoidHomClass F A B] [ContinuousMapClass F A B]` instead. -/
structure ContinuousAddMonoidHomClass (A B : outParam Type*) [AddMonoid A] [AddMonoid B]
[TopologicalSpace A] [TopologicalSpace B] [FunLike F A B]
extends AddMonoidHomClass F A B : Prop where
/-- Proof of the continuity of the map. -/
map_continuous (f : F) : Continuous f
extends AddMonoidHomClass F A B, ContinuousMapClass F A B : Prop

/-- `ContinuousMonoidHomClass F A B` states that `F` is a type of continuous monoid
homomorphisms.

You should also extend this typeclass when you extend `ContinuousMonoidHom`. -/
-- Porting note: Changed A B to outParam to help synthesizing order
@[to_additive]
class ContinuousMonoidHomClass (A B : outParam Type*) [Monoid A] [Monoid B]
Deprecated and changed from a `class` to a `structure`.
Use `[MonoidHomClass F A B] [ContinuousMapClass F A B]` instead. -/
@[to_additive (attr := deprecated (since := "2024-10-08"))]
structure ContinuousMonoidHomClass (A B : outParam Type*) [Monoid A] [Monoid B]
[TopologicalSpace A] [TopologicalSpace B] [FunLike F A B]
extends MonoidHomClass F A B : Prop where
/-- Proof of the continuity of the map. -/
map_continuous (f : F) : Continuous f
extends MonoidHomClass F A B, ContinuousMapClass F A B : Prop

end

Expand All @@ -82,66 +78,66 @@ add_decl_doc ContinuousMonoidHom.toMonoidHom
/-- Reinterpret a `ContinuousAddMonoidHom` as an `AddMonoidHom`. -/
add_decl_doc ContinuousAddMonoidHom.toAddMonoidHom

-- See note [lower instance priority]
@[to_additive]
instance (priority := 100) ContinuousMonoidHomClass.toContinuousMapClass
[FunLike F A B] [ContinuousMonoidHomClass F A B] : ContinuousMapClass F A B :=
{ ‹ContinuousMonoidHomClass F A B› with }
/-- Reinterpret a `ContinuousMonoidHom` as a `ContinuousMap`. -/
add_decl_doc ContinuousMonoidHom.toContinuousMap

/-- Reinterpret a `ContinuousAddMonoidHom` as a `ContinuousMap`. -/
add_decl_doc ContinuousAddMonoidHom.toContinuousMap

namespace ContinuousMonoidHom

variable {A B C D E}

@[to_additive]
instance funLike : FunLike (ContinuousMonoidHom A B) A B where
instance instFunLike : FunLike (ContinuousMonoidHom A B) A B where
coe f := f.toFun
coe_injective' f g h := by
obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := f
obtain ⟨⟨⟨ _ , _ ⟩, _⟩, _⟩ := g
congr

@[to_additive]
instance ContinuousMonoidHomClass : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B where
instance instMonoidHomClass : MonoidHomClass (ContinuousMonoidHom A B) A B where
map_mul f := f.map_mul'
map_one f := f.map_one'

@[to_additive]
instance instContinuousMapClass : ContinuousMapClass (ContinuousMonoidHom A B) A B where
map_continuous f := f.continuous_toFun

@[to_additive (attr := ext)]
theorem ext {f g : ContinuousMonoidHom A B} (h : ∀ x, f x = g x) : f = g :=
DFunLike.ext _ _ h

/-- Reinterpret a `ContinuousMonoidHom` as a `ContinuousMap`. -/
@[to_additive "Reinterpret a `ContinuousAddMonoidHom` as a `ContinuousMap`."]
def toContinuousMap (f : ContinuousMonoidHom A B) : C(A, B) :=
{ f with }

@[to_additive]
theorem toContinuousMap_injective : Injective (toContinuousMap : _ → C(A, B)) := fun f g h =>
ext <| by convert DFunLike.ext_iff.1 h

-- Porting note: Removed simps because given definition is not a constructor application
/-- Construct a `ContinuousMonoidHom` from a `Continuous` `MonoidHom`. -/
@[to_additive "Construct a `ContinuousAddMonoidHom` from a `Continuous` `AddMonoidHom`."]
def mk' (f : A →* B) (hf : Continuous f) : ContinuousMonoidHom A B :=
{ f with continuous_toFun := (hf : Continuous f.toFun)}
@[deprecated (since := "2024-10-08")] protected alias mk' := mk

@[deprecated (since := "2024-10-08")]
protected alias _root_.ContinuousAddMonoidHom.mk' := ContinuousAddMonoidHom.mk

set_option linter.existingAttributeWarning false in
attribute [to_additive existing] ContinuousMonoidHom.mk'

/-- Composition of two continuous homomorphisms. -/
@[to_additive (attr := simps!) "Composition of two continuous homomorphisms."]
def comp (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ContinuousMonoidHom A C :=
mk' (g.toMonoidHom.comp f.toMonoidHom) (g.continuous_toFun.comp f.continuous_toFun)
⟨g.toMonoidHom.comp f.toMonoidHom, (map_continuous g).comp (map_continuous f)⟩

/-- Product of two continuous homomorphisms on the same space. -/
@[to_additive (attr := simps!) prod "Product of two continuous homomorphisms on the same space."]
def prod (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) :
ContinuousMonoidHom A (B × C) :=
mk' (f.toMonoidHom.prod g.toMonoidHom) (f.continuous_toFun.prod_mk g.continuous_toFun)
⟨f.toMonoidHom.prod g.toMonoidHom, f.continuous_toFun.prod_mk g.continuous_toFun⟩

/-- Product of two continuous homomorphisms on different spaces. -/
@[to_additive (attr := simps!) prodMap
"Product of two continuous homomorphisms on different spaces."]
def prodMap (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) :
ContinuousMonoidHom (A × B) (C × D) :=
mk' (f.toMonoidHom.prodMap g.toMonoidHom) (f.continuous_toFun.prodMap g.continuous_toFun)
⟨f.toMonoidHom.prodMap g.toMonoidHom, f.continuous_toFun.prodMap g.continuous_toFun⟩

@[deprecated (since := "2024-10-05")] alias prod_map := prodMap
@[deprecated (since := "2024-10-05")]
Expand All @@ -155,7 +151,7 @@ variable (A B C D E)
/-- The trivial continuous homomorphism. -/
@[to_additive (attr := simps!) "The trivial continuous homomorphism."]
def one : ContinuousMonoidHom A B :=
mk' 1 continuous_const
⟨1, continuous_const⟩

@[to_additive]
instance : Inhabited (ContinuousMonoidHom A B) :=
Expand All @@ -164,19 +160,19 @@ instance : Inhabited (ContinuousMonoidHom A B) :=
/-- The identity continuous homomorphism. -/
@[to_additive (attr := simps!) "The identity continuous homomorphism."]
def id : ContinuousMonoidHom A A :=
mk' (MonoidHom.id A) continuous_id
⟨.id A, continuous_id⟩

/-- The continuous homomorphism given by projection onto the first factor. -/
@[to_additive (attr := simps!)
"The continuous homomorphism given by projection onto the first factor."]
def fst : ContinuousMonoidHom (A × B) A :=
mk' (MonoidHom.fst A B) continuous_fst
⟨MonoidHom.fst A B, continuous_fst⟩

/-- The continuous homomorphism given by projection onto the second factor. -/
@[to_additive (attr := simps!)
"The continuous homomorphism given by projection onto the second factor."]
def snd : ContinuousMonoidHom (A × B) B :=
mk' (MonoidHom.snd A B) continuous_snd
⟨MonoidHom.snd A B, continuous_snd⟩

/-- The continuous homomorphism given by inclusion of the first factor. -/
@[to_additive (attr := simps!)
Expand All @@ -203,12 +199,12 @@ def swap : ContinuousMonoidHom (A × B) (B × A) :=
/-- The continuous homomorphism given by multiplication. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by addition."]
def mul : ContinuousMonoidHom (E × E) E :=
mk' mulMonoidHom continuous_mul
⟨mulMonoidHom, continuous_mul⟩

/-- The continuous homomorphism given by inversion. -/
@[to_additive (attr := simps!) "The continuous homomorphism given by negation."]
def inv : ContinuousMonoidHom E E :=
mk' invMonoidHom continuous_inv
⟨invMonoidHom, continuous_inv⟩

variable {A B C D E}

Expand Down
9 changes: 6 additions & 3 deletions Mathlib/Topology/Algebra/PontryaginDual.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,13 @@ namespace PontryaginDual
open ContinuousMonoidHom

instance : FunLike (PontryaginDual A) A Circle :=
ContinuousMonoidHom.funLike
ContinuousMonoidHom.instFunLike

noncomputable instance : ContinuousMonoidHomClass (PontryaginDual A) A Circle :=
ContinuousMonoidHom.ContinuousMonoidHomClass
noncomputable instance instContinuousMapClass : ContinuousMapClass (PontryaginDual A) A Circle :=
ContinuousMonoidHom.instContinuousMapClass

noncomputable instance instMonoidHomClass : MonoidHomClass (PontryaginDual A) A Circle :=
ContinuousMonoidHom.instMonoidHomClass

/-- `PontryaginDual` is a contravariant functor. -/
noncomputable def map (f : ContinuousMonoidHom A B) :
Expand Down
Loading