Smooth monoid morphisms #
Identity, composition, and their laws for bundled smooth multiplicative and additive monoid morphisms. It also propagates the regularity of multiplicative and additive maps from a group at any one point to the whole group.
def
ContMDiffMonoidMorphism.id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
:
ContMDiffMonoidMorphism I I n G G
The identity smooth monoid morphism.
Instances For
def
ContMDiffAddMonoidMorphism.id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
:
ContMDiffAddMonoidMorphism I I n G G
The identity smooth additive monoid morphism.
Instances For
@[simp]
theorem
ContMDiffMonoidMorphism.coe_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
:
@[simp]
theorem
ContMDiffAddMonoidMorphism.coe_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
:
def
ContMDiffMonoidMorphism.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[Monoid G'']
(ψ : ContMDiffMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffMonoidMorphism I I' n G G')
:
ContMDiffMonoidMorphism I I'' n G G''
Composition of smooth monoid morphisms.
Instances For
def
ContMDiffAddMonoidMorphism.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[AddMonoid G'']
(ψ : ContMDiffAddMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffAddMonoidMorphism I I' n G G')
:
ContMDiffAddMonoidMorphism I I'' n G G''
Composition of smooth additive monoid morphisms.
Instances For
@[simp]
theorem
ContMDiffMonoidMorphism.coe_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[Monoid G'']
(ψ : ContMDiffMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffMonoidMorphism I I' n G G')
:
@[simp]
theorem
ContMDiffAddMonoidMorphism.coe_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[AddMonoid G'']
(ψ : ContMDiffAddMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffAddMonoidMorphism I I' n G G')
:
@[simp]
theorem
ContMDiffMonoidMorphism.id_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
(φ : ContMDiffMonoidMorphism I I' n G G')
:
The identity smooth monoid morphism is a left unit for composition.
@[simp]
theorem
ContMDiffAddMonoidMorphism.id_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
(φ : ContMDiffAddMonoidMorphism I I' n G G')
:
The identity smooth additive monoid morphism is a left unit for composition.
@[simp]
theorem
ContMDiffMonoidMorphism.comp_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
(φ : ContMDiffMonoidMorphism I I' n G G')
:
The identity smooth monoid morphism is a right unit for composition.
@[simp]
theorem
ContMDiffAddMonoidMorphism.comp_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
(φ : ContMDiffAddMonoidMorphism I I' n G G')
:
The identity smooth additive monoid morphism is a right unit for composition.
@[simp]
theorem
ContMDiffMonoidMorphism.comp_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Monoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[Monoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[Monoid G'']
{E''' : Type u_11}
[NormedAddCommGroup E''']
[NormedSpace 𝕜 E''']
{H''' : Type u_12}
[TopologicalSpace H''']
{I''' : ModelWithCorners 𝕜 E''' H'''}
{G''' : Type u_13}
[TopologicalSpace G''']
[ChartedSpace H''' G''']
[Monoid G''']
(χ : ContMDiffMonoidMorphism I'' I''' n G'' G''')
(ψ : ContMDiffMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffMonoidMorphism I I' n G G')
:
Composition of smooth monoid morphisms is associative.
@[simp]
theorem
ContMDiffAddMonoidMorphism.comp_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[AddMonoid G]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G' : Type u_7}
[TopologicalSpace G']
[ChartedSpace H' G']
[AddMonoid G']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{G'' : Type u_10}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[AddMonoid G'']
{E''' : Type u_11}
[NormedAddCommGroup E''']
[NormedSpace 𝕜 E''']
{H''' : Type u_12}
[TopologicalSpace H''']
{I''' : ModelWithCorners 𝕜 E''' H'''}
{G''' : Type u_13}
[TopologicalSpace G''']
[ChartedSpace H''' G''']
[AddMonoid G''']
(χ : ContMDiffAddMonoidMorphism I'' I''' n G'' G''')
(ψ : ContMDiffAddMonoidMorphism I' I'' n G' G'')
(φ : ContMDiffAddMonoidMorphism I I' n G G')
:
Composition of smooth additive monoid morphisms is associative.
theorem
TauCeti.contMDiff_of_contMDiffAt_mulHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
{G' : Type u_7}
[Mul G']
[TopologicalSpace G']
[ChartedSpace H' G']
{F : Type u_8}
[FunLike F G G']
[MulHomClass F G G']
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n G G]
[ContMDiffConstSMul I' n G' G']
(f : F)
{a : G}
(hf : ContMDiffAt I I' n (⇑f) a)
:
ContMDiff I I' n ⇑f
A multiplicative map from a group that is C^n at one point is C^n everywhere.
This is a smooth generalization of Mathlib's continuous_of_continuousAt_one, with regularity
assumed at an arbitrary basepoint.
The map need not preserve an identity. Only the individual left translations on the source
and target must be C^n, as expressed by ContMDiffConstSMul for multiplication acting on
itself. In particular, smooth multiplication suffices; smooth inversion is not required.
theorem
TauCeti.contMDiff_of_contMDiffAt_addHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[AddGroup G]
[TopologicalSpace G]
[ChartedSpace H G]
{G' : Type u_7}
[Add G']
[TopologicalSpace G']
[ChartedSpace H' G']
{F : Type u_8}
[FunLike F G G']
[AddHomClass F G G']
{n : WithTop ℕ∞}
[ContMDiffConstVAdd I n G G]
[ContMDiffConstVAdd I' n G' G']
(f : F)
{a : G}
(hf : ContMDiffAt I I' n (⇑f) a)
:
ContMDiff I I' n ⇑f
An additive map from an additive group that is C^n at one point is C^n everywhere.
This is a smooth generalization of Mathlib's continuous_of_continuousAt_zero, with regularity
assumed at an arbitrary basepoint.
The map need not preserve a zero. Only the individual left translations on the source
and target must be C^n, as expressed by ContMDiffConstVAdd for addition acting on
itself. In particular, smooth addition suffices; smooth negation is not required.