Mathlib.Topology.Algebra.SeparationQuotient.Basic

SeparationQuotient.instSMul instance

: SMul M (SeparationQuotient X)

Full source

@[to_additive]
instance instSMul : SMul M (SeparationQuotient X) where
  smul c := Quotient.map' (c • ·) fun _ _ h ↦ h.const_smul c

Scalar Multiplication on the Separation Quotient

Informal description

For any topological space $X$ with a scalar multiplication action by $M$, the separation quotient $\text{SeparationQuotient } X$ inherits a scalar multiplication structure from $X$, defined by $c \cdot [x] = [c \cdot x]$ for any $c \in M$ and $x \in X$, where $[x]$ denotes the equivalence class of $x$ in the separation quotient.

SeparationQuotient.mk_smul theorem

(c : M) (x : X) : mk (c • x) = c • mk x

Full source

@[to_additive (attr := simp)]
theorem mk_smul (c : M) (x : X) : mk (c • x) = c • mk x := rfl

Compatibility of Scalar Multiplication with Separation Quotient Projection

Informal description

For any scalar $c \in M$ and any point $x \in X$, the projection map $\text{mk}$ from $X$ to its separation quotient satisfies $\text{mk}(c \cdot x) = c \cdot \text{mk}(x)$, where the scalar multiplication on the quotient is defined as $c \cdot [x] = [c \cdot x]$.

SeparationQuotient.instContinuousConstSMul instance

: ContinuousConstSMul M (SeparationQuotient X)

Full source

@[to_additive]
instance instContinuousConstSMul : ContinuousConstSMul M (SeparationQuotient X) where
  continuous_const_smul c := isQuotientMap_mk.continuous_iff.2 <|
    continuous_mk.comp <| continuous_const_smul c

Continuous Scalar Multiplication on the Separation Quotient

Informal description

For any topological space $X$ with a scalar multiplication action by $M$ such that the map $x \mapsto c \cdot x$ is continuous for each fixed $c \in M$, the separation quotient $\text{SeparationQuotient } X$ inherits a continuous scalar multiplication structure, where the action is defined by $c \cdot [x] = [c \cdot x]$ for $c \in M$ and $x \in X$.

SeparationQuotient.instIsPretransitiveSMul instance

[MulAction.IsPretransitive M X] : MulAction.IsPretransitive M (SeparationQuotient X)

Full source

@[to_additive]
instance instIsPretransitiveSMul [MulAction.IsPretransitive M X] :
    MulAction.IsPretransitive M (SeparationQuotient X) where
  exists_smul_eq := surjective_mk.forall₂.2 fun x y ↦
    (MulAction.exists_smul_eq M x y).imp fun _ ↦ congr_arg mk

Pretransitivity of Induced Group Action on Separation Quotient

Informal description

If a group action of $M$ on a topological space $X$ is pretransitive, then the induced action on the separation quotient $\text{SeparationQuotient } X$ is also pretransitive. That is, for any two equivalence classes $[x], [y] \in \text{SeparationQuotient } X$, there exists an element $m \in M$ such that $m \cdot [x] = [y]$.

SeparationQuotient.instIsCentralScalar instance

[SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (SeparationQuotient X)

Full source

@[to_additive]
instance instIsCentralScalar [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] :
    IsCentralScalar M (SeparationQuotient X) where
  op_smul_eq_smul a := surjective_mk.forall.2 (congr_arg mk <| op_smul_eq_smul a ·)

Central Scalar Multiplication on the Separation Quotient

Informal description

For any topological space $X$ with a scalar multiplication action by $M$ that is central (i.e., the left and right actions coincide), the induced scalar multiplication on the separation quotient $\text{SeparationQuotient } X$ is also central. This means that for any $c \in M$ and $[x] \in \text{SeparationQuotient } X$, the left action $c \cdot [x]$ and the right action $[x] \cdot c$ are equal.

SeparationQuotient.instSMulCommClass instance

[ContinuousConstSMul N X] [SMulCommClass M N X] : SMulCommClass M N (SeparationQuotient X)

Full source

@[to_additive]
instance instSMulCommClass [ContinuousConstSMul N X] [SMulCommClass M N X] :
    SMulCommClass M N (SeparationQuotient X) :=
  surjective_mk.smulCommClass mk_smul mk_smul

Commutativity of Induced Scalar Actions on Separation Quotient

Informal description

For any topological space $X$ with commuting scalar multiplication actions by $M$ and $N$, where the action of $N$ is continuous in the second variable, the induced scalar multiplication actions on the separation quotient $\text{SeparationQuotient } X$ also commute. That is, for any $m \in M$, $n \in N$, and $[x] \in \text{SeparationQuotient } X$, we have $m \cdot (n \cdot [x]) = n \cdot (m \cdot [x])$.

SeparationQuotient.instIsScalarTower instance

[SMul M N] [ContinuousConstSMul N X] [IsScalarTower M N X] : IsScalarTower M N (SeparationQuotient X)

Full source

@[to_additive]
instance instIsScalarTower [SMul M N] [ContinuousConstSMul N X] [IsScalarTower M N X] :
    IsScalarTower M N (SeparationQuotient X) where
  smul_assoc a b := surjective_mk.forall.2 fun x ↦ congr_arg mk <| smul_assoc a b x

Scalar Tower Property on the Separation Quotient

Informal description

For any topological space $X$ with a scalar multiplication action by $M$ and $N$, where the action of $N$ is continuous in the second variable, and the scalar multiplication satisfies the tower property $M \cdot (N \cdot x) = (M \cdot N) \cdot x$ for all $x \in X$, the separation quotient $\text{SeparationQuotient } X$ also inherits the tower property for scalar multiplication.

SeparationQuotient.instContinuousSMul instance

 {M X : Type*} [SMul M X] [TopologicalSpace M] [TopologicalSpace X] [ContinuousSMul M X] :
  ContinuousSMul M (SeparationQuotient X)

Full source

instance instContinuousSMul {M X : Type*} [SMul M X] [TopologicalSpace M] [TopologicalSpace X]
    [ContinuousSMul M X] : ContinuousSMul M (SeparationQuotient X) where
  continuous_smul := by
    rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).isQuotientMap.continuous_iff]
    exact continuous_mk.comp continuous_smul

Continuous Scalar Multiplication on the Separation Quotient

Informal description

For any topological space $X$ with a scalar multiplication action by $M$ that is jointly continuous (i.e., the map $(c, x) \mapsto c \cdot x$ is continuous), the separation quotient $\text{SeparationQuotient } X$ inherits a jointly continuous scalar multiplication structure from $X$, defined by $c \cdot [x] = [c \cdot x]$ for any $c \in M$ and $x \in X$, where $[x]$ denotes the equivalence class of $x$ in the separation quotient.

SeparationQuotient.instSMulZeroClass instance

 {M X : Type*} [Zero X] [SMulZeroClass M X] [TopologicalSpace X] [ContinuousConstSMul M X] :
  SMulZeroClass M (SeparationQuotient X)

Full source

instance instSMulZeroClass {M X : Type*} [Zero X] [SMulZeroClass M X] [TopologicalSpace X]
    [ContinuousConstSMul M X] : SMulZeroClass M (SeparationQuotient X) :=
  ZeroHom.smulZeroClass ⟨mk, mk_zero⟩ mk_smul

Scalar Multiplication Preserving Zero on the Separation Quotient

Informal description

For any topological space $X$ with a zero element and a scalar multiplication action by $M$ that preserves zero, if the scalar multiplication is continuous in the second argument for each fixed scalar, then the separation quotient $\text{SeparationQuotient } X$ inherits a scalar multiplication structure that also preserves zero.

SeparationQuotient.instMulAction instance

 {M X : Type*} [Monoid M] [MulAction M X] [TopologicalSpace X] [ContinuousConstSMul M X] :
  MulAction M (SeparationQuotient X)

Full source

@[to_additive]
instance instMulAction {M X : Type*} [Monoid M] [MulAction M X] [TopologicalSpace X]
    [ContinuousConstSMul M X] : MulAction M (SeparationQuotient X) :=
  surjective_mk.mulAction mk mk_smul

Multiplicative Action on the Separation Quotient of a Topological Space

Informal description

For any monoid $M$ acting on a topological space $X$ with continuous scalar multiplication in the second variable, the separation quotient $\text{SeparationQuotient } X$ inherits a multiplicative action structure from $X$, defined by $c \cdot [x] = [c \cdot x]$ for any $c \in M$ and $x \in X$, where $[x]$ denotes the equivalence class of $x$ in the separation quotient.

SeparationQuotient.instMul instance

[Mul M] [ContinuousMul M] : Mul (SeparationQuotient M)

Full source

@[to_additive]
instance instMul [Mul M] [ContinuousMul M] : Mul (SeparationQuotient M) where
  mul := Quotient.map₂ (· * ·) fun _ _ h₁ _ _ h₂ ↦ Inseparable.mul h₁ h₂

Multiplication on the Separation Quotient of a Topological Monoid

Informal description

For any topological space $M$ equipped with a continuous multiplication operation, the separation quotient $\text{SeparationQuotient } M$ inherits a multiplication operation defined by lifting the original multiplication through the quotient map.

SeparationQuotient.mk_mul theorem

[Mul M] [ContinuousMul M] (a b : M) : mk (a * b) = mk a * mk b

Full source

@[to_additive (attr := simp)]
theorem mk_mul [Mul M] [ContinuousMul M] (a b : M) : mk (a * b) = mk a * mk b := rfl

Projection Preserves Multiplication in Separation Quotient

Informal description

Let $M$ be a topological space equipped with a continuous multiplication operation. For any elements $a, b \in M$, the projection of their product $a * b$ to the separation quotient equals the product of their projections, i.e., $\text{mk}(a * b) = \text{mk}(a) * \text{mk}(b)$.

SeparationQuotient.instContinuousMul instance

[Mul M] [ContinuousMul M] : ContinuousMul (SeparationQuotient M)

Full source

@[to_additive]
instance instContinuousMul [Mul M] [ContinuousMul M] : ContinuousMul (SeparationQuotient M) where
  continuous_mul := isQuotientMap_prodMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_mul

Continuity of Multiplication on the Separation Quotient of a Topological Monoid

Informal description

For any topological space $M$ equipped with a continuous multiplication operation, the induced multiplication on the separation quotient $\text{SeparationQuotient } M$ is also continuous.

SeparationQuotient.instCommMagma instance

[CommMagma M] [ContinuousMul M] : CommMagma (SeparationQuotient M)

Full source

@[to_additive]
instance instCommMagma [CommMagma M] [ContinuousMul M] : CommMagma (SeparationQuotient M) :=
  surjective_mk.commMagma mk mk_mul

Commutative Magma Structure on Separation Quotient of Topological Commutative Magma

Informal description

For any topological space $M$ equipped with a continuous commutative multiplication operation, the separation quotient $\text{SeparationQuotient } M$ inherits a commutative magma structure, where the multiplication is defined by lifting the original multiplication through the quotient map.

SeparationQuotient.instSemigroup instance

[Semigroup M] [ContinuousMul M] : Semigroup (SeparationQuotient M)

Full source

@[to_additive]
instance instSemigroup [Semigroup M] [ContinuousMul M] : Semigroup (SeparationQuotient M) :=
  surjective_mk.semigroup mk mk_mul

Semigroup Structure on the Separation Quotient of a Topological Semigroup

Informal description

For any topological semigroup $M$ with continuous multiplication, the separation quotient $\text{SeparationQuotient } M$ inherits a semigroup structure from $M$. The multiplication on the quotient is defined by lifting the original multiplication through the quotient map.

SeparationQuotient.instCommSemigroup instance

[CommSemigroup M] [ContinuousMul M] : CommSemigroup (SeparationQuotient M)

Full source

@[to_additive]
instance instCommSemigroup [CommSemigroup M] [ContinuousMul M] :
    CommSemigroup (SeparationQuotient M) :=
  surjective_mk.commSemigroup mk mk_mul

Commutative Semigroup Structure on the Separation Quotient

Informal description

For any commutative semigroup $M$ with a continuous multiplication operation, the separation quotient $\text{SeparationQuotient } M$ inherits a commutative semigroup structure.

SeparationQuotient.instMulOneClass instance

[MulOneClass M] [ContinuousMul M] : MulOneClass (SeparationQuotient M)

Full source

@[to_additive]
instance instMulOneClass [MulOneClass M] [ContinuousMul M] :
    MulOneClass (SeparationQuotient M) :=
  surjective_mk.mulOneClass mk mk_one mk_mul

MulOneClass Structure on the Separation Quotient of a Topological MulOneClass

Informal description

For any topological space $M$ equipped with a continuous multiplication operation and a distinguished element $1$ forming a `MulOneClass`, the separation quotient $\operatorname{SeparationQuotient} M$ inherits a `MulOneClass` structure where the multiplication and identity are defined by lifting the original operations through the quotient map.

SeparationQuotient.mkMonoidHom definition

[MulOneClass M] [ContinuousMul M] : M →* SeparationQuotient M

Full source

/-- `SeparationQuotient.mk` as a `MonoidHom`. -/
@[to_additive (attr := simps) "`SeparationQuotient.mk` as an `AddMonoidHom`."]
def mkMonoidHom [MulOneClass M] [ContinuousMul M] : M →* SeparationQuotient M where
  toFun := mk
  map_mul' := mk_mul
  map_one' := mk_one

Monoid homomorphism from a topological monoid to its separation quotient

Informal description

The function that maps an element of a topological monoid $ M $ with continuous multiplication to its equivalence class in the separation quotient $ \text{SeparationQuotient } M $, viewed as a monoid homomorphism. This homomorphism preserves the multiplication and identity elements of $ M $.

SeparationQuotient.instNSmul instance

[AddMonoid M] [ContinuousAdd M] : SMul ℕ (SeparationQuotient M)

Full source

instance (priority := 900) instNSmul [AddMonoid M] [ContinuousAdd M] :
    SMul ℕ (SeparationQuotient M) :=
  inferInstance

Natural Scalar Multiplication on the Separation Quotient of an Additive Monoid

Informal description

For any additive monoid $M$ with a topological space structure and continuous addition, the separation quotient $\text{SeparationQuotient } M$ inherits a scalar multiplication structure by natural numbers from $M$, defined by $n \cdot [x] = [n \cdot x]$ for any $n \in \mathbb{N}$ and $x \in M$, where $[x]$ denotes the equivalence class of $x$ in the separation quotient.

SeparationQuotient.instPow instance

[Monoid M] [ContinuousMul M] : Pow (SeparationQuotient M) ℕ

Full source

@[to_additive existing instNSmul]
instance instPow [Monoid M] [ContinuousMul M] : Pow (SeparationQuotient M) ℕ where
  pow x n := Quotient.map' (s₁ := inseparableSetoid M) (· ^ n) (fun _ _ h ↦ Inseparable.pow h n) x

Power Operation on the Separation Quotient of a Topological Monoid

Informal description

For any topological monoid $M$ with continuous multiplication, the separation quotient $\text{SeparationQuotient } M$ inherits a natural power operation $\cdot^n$ for natural numbers $n$.

SeparationQuotient.mk_pow theorem

[Monoid M] [ContinuousMul M] (x : M) (n : ℕ) : mk (x ^ n) = (mk x) ^ n

Full source

@[to_additive, simp] -- `mk_nsmul` is not a `simp` lemma because we have `mk_smul`
theorem mk_pow [Monoid M] [ContinuousMul M] (x : M) (n : ℕ) : mk (x ^ n) = (mk x) ^ n := rfl

Power Operation Commutes with Separation Quotient Projection

Informal description

Let $M$ be a topological monoid with continuous multiplication. For any element $x \in M$ and natural number $n \in \mathbb{N}$, the projection of $x^n$ to the separation quotient of $M$ equals the $n$-th power of the projection of $x$, i.e., $\pi(x^n) = (\pi x)^n$, where $\pi \colon M \to \text{SeparationQuotient } M$ is the quotient map.

SeparationQuotient.instMonoid instance

[Monoid M] [ContinuousMul M] : Monoid (SeparationQuotient M)

Full source

@[to_additive]
instance instMonoid [Monoid M] [ContinuousMul M] : Monoid (SeparationQuotient M) :=
  surjective_mk.monoid mk mk_one mk_mul mk_pow

Monoid Structure on the Separation Quotient of a Topological Monoid

Informal description

For any topological monoid $M$ with continuous multiplication, the separation quotient $\text{SeparationQuotient } M$ inherits a monoid structure, where the multiplication and identity are defined by lifting the original operations through the quotient map.

SeparationQuotient.instCommMonoid instance

[CommMonoid M] [ContinuousMul M] : CommMonoid (SeparationQuotient M)

Full source

@[to_additive]
instance instCommMonoid [CommMonoid M] [ContinuousMul M] : CommMonoid (SeparationQuotient M) :=
  surjective_mk.commMonoid mk mk_one mk_mul mk_pow

Commutative Monoid Structure on the Separation Quotient of a Topological Commutative Monoid

Informal description

For any topological space $M$ equipped with a commutative monoid structure and continuous multiplication, the separation quotient $\operatorname{SeparationQuotient} M$ inherits a commutative monoid structure where the multiplication is defined by lifting the original multiplication through the quotient map.

SeparationQuotient.instInv instance

[Inv G] [ContinuousInv G] : Inv (SeparationQuotient G)

Full source

@[to_additive]
instance instInv [Inv G] [ContinuousInv G] : Inv (SeparationQuotient G) where
  inv := Quotient.map' (·⁻¹) fun _ _ ↦ Inseparable.inv

Inversion Operation on the Separation Quotient of a Topological Group

Informal description

For any topological space $G$ equipped with a continuous inversion operation, the separation quotient of $G$ inherits an inversion operation. This means that if $G$ has a continuous map $x \mapsto x^{-1}$, then the quotient space $\text{SeparationQuotient } G$ also has a well-defined inversion operation that is compatible with the quotient map.

SeparationQuotient.mk_inv theorem

[Inv G] [ContinuousInv G] (x : G) : mk x⁻¹ = (mk x)⁻¹

Full source

@[to_additive (attr := simp)]
theorem mk_inv [Inv G] [ContinuousInv G] (x : G) : mk x⁻¹ = (mk x)⁻¹ := rfl

Inversion Commutes with Separation Quotient Projection

Informal description

Let $G$ be a topological space equipped with a continuous inversion operation $x \mapsto x^{-1}$. For any $x \in G$, the projection of the inverse $x^{-1}$ to the separation quotient of $G$ equals the inverse of the projection of $x$, i.e., $\text{mk}(x^{-1}) = (\text{mk}(x))^{-1}$.

SeparationQuotient.instContinuousInv instance

[Inv G] [ContinuousInv G] : ContinuousInv (SeparationQuotient G)

Full source

@[to_additive]
instance instContinuousInv [Inv G] [ContinuousInv G] : ContinuousInv (SeparationQuotient G) where
  continuous_inv := isQuotientMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_inv

Continuity of Inversion on the Separation Quotient

Informal description

For any topological space $G$ equipped with a continuous inversion operation, the separation quotient $\text{SeparationQuotient } G$ inherits a continuous inversion operation. That is, if $G$ has a continuous map $x \mapsto x^{-1}$, then the inversion operation on $\text{SeparationQuotient } G$ is also continuous.

SeparationQuotient.instInvolutiveInv instance

[InvolutiveInv G] [ContinuousInv G] : InvolutiveInv (SeparationQuotient G)

Full source

@[to_additive]
instance instInvolutiveInv [InvolutiveInv G] [ContinuousInv G] :
    InvolutiveInv (SeparationQuotient G) :=
  surjective_mk.involutiveInv mk mk_inv

Involutive Inversion on the Separation Quotient

Informal description

For any topological space $G$ with a continuous involutive inversion operation (i.e., $(x^{-1})^{-1} = x$ for all $x \in G$), the separation quotient $\text{SeparationQuotient } G$ also inherits an involutive inversion operation.

SeparationQuotient.instInvOneClass instance

[InvOneClass G] [ContinuousInv G] : InvOneClass (SeparationQuotient G)

Full source

@[to_additive]
instance instInvOneClass [InvOneClass G] [ContinuousInv G] :
    InvOneClass (SeparationQuotient G) where
  inv_one := congr_arg mk inv_one

Involution and Identity Preservation in the Separation Quotient

Informal description

For any topological space $G$ with a continuous inversion operation and a distinguished element $1$ satisfying the properties of an `InvOneClass` (i.e., $1^{-1} = 1$), the separation quotient $\operatorname{SeparationQuotient} G$ inherits an `InvOneClass` structure. This means that the image of $1$ under the quotient map is preserved under inversion in the quotient space.

SeparationQuotient.instDiv instance

[Div G] [ContinuousDiv G] : Div (SeparationQuotient G)

Full source

@[to_additive]
instance instDiv [Div G] [ContinuousDiv G] : Div (SeparationQuotient G) where
  div := Quotient.map₂ (· / ·) fun _ _ h₁ _ _ h₂ ↦ (Inseparable.prod h₁ h₂).map continuous_div'

Division Operation on the Separation Quotient of a Topological Space with Continuous Division

Informal description

For any topological space $G$ equipped with a continuous division operation, the separation quotient of $G$ inherits a division operation.

SeparationQuotient.mk_div theorem

[Div G] [ContinuousDiv G] (x y : G) : mk (x / y) = mk x / mk y

Full source

@[to_additive (attr := simp)]
theorem mk_div [Div G] [ContinuousDiv G] (x y : G) : mk (x / y) = mk x / mk y := rfl

Quotient Map Preserves Division in Separation Quotient

Informal description

Let $G$ be a topological space equipped with a continuous division operation. For any elements $x, y \in G$, the projection of the quotient $x / y$ under the separation quotient map equals the division of the projections of $x$ and $y$ in the separation quotient, i.e., $\text{mk}(x / y) = \text{mk}(x) / \text{mk}(y)$.

SeparationQuotient.instContinuousDiv instance

[Div G] [ContinuousDiv G] : ContinuousDiv (SeparationQuotient G)

Full source

@[to_additive]
instance instContinuousDiv [Div G] [ContinuousDiv G] : ContinuousDiv (SeparationQuotient G) where
  continuous_div' := isQuotientMap_prodMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_div'

Continuous Division on the Separation Quotient of a Topological Space with Continuous Division

Informal description

For any topological space $G$ equipped with a continuous division operation, the separation quotient of $G$ inherits a continuous division operation.

SeparationQuotient.instZSMul instance

[AddGroup G] [IsTopologicalAddGroup G] : SMul ℤ (SeparationQuotient G)

Full source

instance instZSMul [AddGroup G] [IsTopologicalAddGroup G] : SMul ℤ (SeparationQuotient G) :=
  inferInstance

Integer Scalar Multiplication on the Separation Quotient of a Topological Additive Group

Informal description

For any topological additive group $G$, the separation quotient $\text{SeparationQuotient } G$ inherits a scalar multiplication structure by integers from $G$. Specifically, for any $n \in \mathbb{Z}$ and $x \in G$, the equivalence class of $n \cdot x$ in the separation quotient is equal to $n$ times the equivalence class of $x$.

SeparationQuotient.instZPow instance

[Group G] [IsTopologicalGroup G] : Pow (SeparationQuotient G) ℤ

Full source

@[to_additive existing]
instance instZPow [Group G] [IsTopologicalGroup G] : Pow (SeparationQuotient G) ℤ where
  pow x n := Quotient.map' (s₁ := inseparableSetoid G) (· ^ n) (fun _ _ h ↦ Inseparable.zpow h n) x

Integer Powers on the Separation Quotient of a Topological Group

Informal description

For any topological group $G$, the separation quotient $\text{SeparationQuotient } G$ inherits a power operation with integer exponents from $G$. Specifically, if $G$ is a group with a topology making the group operations continuous, then the quotient map preserves the integer power operation: for any $x \in G$ and $n \in \mathbb{Z}$, the equivalence class of $x^n$ in the separation quotient is equal to the $n$-th power of the equivalence class of $x$.

SeparationQuotient.mk_zpow theorem

[Group G] [IsTopologicalGroup G] (x : G) (n : ℤ) : mk (x ^ n) = (mk x) ^ n

Full source

@[to_additive, simp] -- `mk_zsmul` is not a `simp` lemma because we have `mk_smul`
theorem mk_zpow [Group G] [IsTopologicalGroup G] (x : G) (n : ℤ) : mk (x ^ n) = (mk x) ^ n := rfl

Compatibility of Integer Powers with Separation Quotient Projection

Informal description

Let $G$ be a topological group. For any element $x \in G$ and any integer $n \in \mathbb{Z}$, the projection of $x^n$ to the separation quotient of $G$ equals the $n$-th power of the projection of $x$, i.e., \[ \text{mk}(x^n) = (\text{mk}(x))^n. \]

SeparationQuotient.instGroup instance

[Group G] [IsTopologicalGroup G] : Group (SeparationQuotient G)

Full source

@[to_additive]
instance instGroup [Group G] [IsTopologicalGroup G] : Group (SeparationQuotient G) :=
  surjective_mk.group mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow

Group Structure on the Separation Quotient of a Topological Group

Informal description

For any topological group $G$, the separation quotient $\operatorname{SeparationQuotient} G$ inherits a group structure from $G$. The group operations on the quotient are defined by lifting the original group operations through the quotient map, and they are compatible with the quotient topology.

SeparationQuotient.instCommGroup instance

[CommGroup G] [IsTopologicalGroup G] : CommGroup (SeparationQuotient G)

Full source

@[to_additive]
instance instCommGroup [CommGroup G] [IsTopologicalGroup G] : CommGroup (SeparationQuotient G) :=
  surjective_mk.commGroup mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow

Commutative Group Structure on the Separation Quotient of a Topological Group

Informal description

For any commutative topological group $G$, the separation quotient $\operatorname{SeparationQuotient} G$ inherits a commutative group structure from $G$.

SeparationQuotient.instIsTopologicalGroup instance

[Group G] [IsTopologicalGroup G] : IsTopologicalGroup (SeparationQuotient G)

Full source

@[to_additive]
instance instIsTopologicalGroup [Group G] [IsTopologicalGroup G] :
    IsTopologicalGroup (SeparationQuotient G) where

Topological Group Structure on the Separation Quotient of a Topological Group

Informal description

For any topological group $G$, the separation quotient $\operatorname{SeparationQuotient} G$ inherits the structure of a topological group. This means that the group operations (multiplication and inversion) on the quotient space are continuous with respect to the quotient topology.

SeparationQuotient.instIsUniformGroup instance

{G : Type*} [Group G] [UniformSpace G] [IsUniformGroup G] : IsUniformGroup (SeparationQuotient G)

Full source

@[to_additive]
instance instIsUniformGroup {G : Type*} [Group G] [UniformSpace G] [IsUniformGroup G] :
    IsUniformGroup (SeparationQuotient G) where
  uniformContinuous_div := by
    rw [uniformContinuous_dom₂]
    exact uniformContinuous_mk.comp uniformContinuous_div

Uniform Group Structure on the Separation Quotient of a Uniform Group

Informal description

For any group $G$ equipped with a uniform space structure that makes it a uniform group, the separation quotient $\operatorname{SeparationQuotient} G$ inherits a uniform group structure. This means that the group operations (multiplication and inversion) on the quotient are uniformly continuous with respect to the quotient uniformity.

SeparationQuotient.instMulZeroClass instance

[MulZeroClass M₀] [ContinuousMul M₀] : MulZeroClass (SeparationQuotient M₀)

Full source

instance instMulZeroClass [MulZeroClass M₀] [ContinuousMul M₀] :
    MulZeroClass (SeparationQuotient M₀) :=
  surjective_mk.mulZeroClass mk mk_zero mk_mul

`MulZeroClass` Structure on the Separation Quotient of a Topological `MulZeroClass`

Informal description

For any topological space $M₀$ equipped with a continuous multiplication operation and a zero element that forms a `MulZeroClass`, the separation quotient $\text{SeparationQuotient } M₀$ inherits a `MulZeroClass` structure, where the multiplication and zero are defined by lifting the original operations through the quotient map.

SeparationQuotient.instSemigroupWithZero instance

[SemigroupWithZero M₀] [ContinuousMul M₀] : SemigroupWithZero (SeparationQuotient M₀)

Full source

instance instSemigroupWithZero [SemigroupWithZero M₀] [ContinuousMul M₀] :
    SemigroupWithZero (SeparationQuotient M₀) :=
  surjective_mk.semigroupWithZero mk mk_zero mk_mul

Semigroup-with-zero Structure on Separation Quotient of a Topological Semigroup-with-zero

Informal description

For any topological space $M₀$ equipped with a semigroup-with-zero structure and continuous multiplication, the separation quotient $\text{SeparationQuotient } M₀$ inherits a semigroup-with-zero structure where the multiplication is defined by lifting the original multiplication through the quotient map.

SeparationQuotient.instMulZeroOneClass instance

[MulZeroOneClass M₀] [ContinuousMul M₀] : MulZeroOneClass (SeparationQuotient M₀)

Full source

instance instMulZeroOneClass [MulZeroOneClass M₀] [ContinuousMul M₀] :
    MulZeroOneClass (SeparationQuotient M₀) :=
  surjective_mk.mulZeroOneClass mk mk_zero mk_one mk_mul

`MulZeroOneClass` Structure on the Separation Quotient of a Topological `MulZeroOneClass` Space

Informal description

For any topological space $M₀$ equipped with a continuous multiplication operation and a distinguished element $1$ satisfying the properties of a `MulZeroOneClass`, the separation quotient $\operatorname{SeparationQuotient} M₀$ inherits a `MulZeroOneClass` structure. This means that the quotient space has a multiplication operation, a zero element, and a one element, with the usual algebraic properties (e.g., $0 \cdot x = 0$ and $1 \cdot x = x$) preserved under the quotient map.

SeparationQuotient.instMonoidWithZero instance

[MonoidWithZero M₀] [ContinuousMul M₀] : MonoidWithZero (SeparationQuotient M₀)

Full source

instance instMonoidWithZero [MonoidWithZero M₀] [ContinuousMul M₀] :
    MonoidWithZero (SeparationQuotient M₀) :=
  surjective_mk.monoidWithZero mk mk_zero mk_one mk_mul mk_pow

Monoid-with-zero Structure on the Separation Quotient of a Topological Monoid-with-zero

Informal description

For any topological monoid with zero $M₀$ where the multiplication operation is continuous, the separation quotient $\text{SeparationQuotient } M₀$ inherits a monoid-with-zero structure. This means the quotient space has an associative multiplication operation with an identity element $1$ and a zero element $0$, satisfying $0 \cdot x = x \cdot 0 = 0$ for all $x$.

SeparationQuotient.instCommMonoidWithZero instance

[CommMonoidWithZero M₀] [ContinuousMul M₀] : CommMonoidWithZero (SeparationQuotient M₀)

Full source

instance instCommMonoidWithZero [CommMonoidWithZero M₀] [ContinuousMul M₀] :
    CommMonoidWithZero (SeparationQuotient M₀) :=
  surjective_mk.commMonoidWithZero mk mk_zero mk_one mk_mul mk_pow

Commutative Monoid with Zero Structure on Separation Quotient

Informal description

For any topological space $M₀$ that is a commutative monoid with zero and has continuous multiplication, the separation quotient $\operatorname{SeparationQuotient} M₀$ inherits a commutative monoid with zero structure. The multiplication operation on the quotient is defined by lifting the original continuous multiplication through the quotient map, preserving commutativity and the properties of the zero element.

SeparationQuotient.instDistrib instance

[Distrib R] [ContinuousMul R] [ContinuousAdd R] : Distrib (SeparationQuotient R)

Full source

instance instDistrib [Distrib R] [ContinuousMul R] [ContinuousAdd R] :
    Distrib (SeparationQuotient R) :=
  surjective_mk.distrib mk mk_add mk_mul

Distributive Structure on the Separation Quotient of a Topological Space

Informal description

For any topological space $R$ equipped with continuous multiplication and addition operations that satisfy the distributive property, the separation quotient $\text{SeparationQuotient } R$ inherits a distributive structure where the operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instLeftDistribClass instance

[Mul R] [Add R] [LeftDistribClass R] [ContinuousMul R] [ContinuousAdd R] : LeftDistribClass (SeparationQuotient R)

Full source

instance instLeftDistribClass [Mul R] [Add R] [LeftDistribClass R]
    [ContinuousMul R] [ContinuousAdd R] :
    LeftDistribClass (SeparationQuotient R) :=
  surjective_mk.leftDistribClass mk mk_add mk_mul

Left Distributive Structure on the Separation Quotient of a Topological Space

Informal description

For any topological space $R$ equipped with continuous multiplication and addition operations that satisfy the left distributive property $a \cdot (b + c) = a \cdot b + a \cdot c$, the separation quotient $\text{SeparationQuotient } R$ inherits a left distributive structure where the operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instRightDistribClass instance

[Mul R] [Add R] [RightDistribClass R] [ContinuousMul R] [ContinuousAdd R] : RightDistribClass (SeparationQuotient R)

Full source

instance instRightDistribClass [Mul R] [Add R] [RightDistribClass R]
    [ContinuousMul R] [ContinuousAdd R] :
    RightDistribClass (SeparationQuotient R) :=
  surjective_mk.rightDistribClass mk mk_add mk_mul

Right Distributive Structure on Separation Quotient

Informal description

For any topological space $R$ equipped with continuous multiplication and addition operations that satisfy the right distributive property $(a + b) \cdot c = a \cdot c + b \cdot c$, the separation quotient $\text{SeparationQuotient}\, R$ inherits a right distributive structure. The operations on the quotient are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonUnitalnonAssocSemiring instance

[NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : NonUnitalNonAssocSemiring (SeparationQuotient R)

Full source

instance instNonUnitalnonAssocSemiring [NonUnitalNonAssocSemiring R]
    [IsTopologicalSemiring R] : NonUnitalNonAssocSemiring (SeparationQuotient R) :=
  surjective_mk.nonUnitalNonAssocSemiring mk mk_zero mk_add mk_mul mk_smul

Non-Unital Non-Associative Semiring Structure on Separation Quotient

Informal description

For any topological space $R$ equipped with a non-unital non-associative semiring structure and continuous addition and multiplication operations, the separation quotient $\text{SeparationQuotient}\, R$ inherits a non-unital non-associative semiring structure. The operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonUnitalSemiring instance

[NonUnitalSemiring R] [IsTopologicalSemiring R] : NonUnitalSemiring (SeparationQuotient R)

Full source

instance instNonUnitalSemiring [NonUnitalSemiring R] [IsTopologicalSemiring R] :
    NonUnitalSemiring (SeparationQuotient R) :=
  surjective_mk.nonUnitalSemiring mk mk_zero mk_add mk_mul mk_smul

Non-Unital Semiring Structure on the Separation Quotient of a Topological Non-Unital Semiring

Informal description

For any topological space $R$ equipped with a non-unital semiring structure where the addition and multiplication operations are continuous, the separation quotient $\text{SeparationQuotient}\, R$ inherits a non-unital semiring structure. The operations on the quotient are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNatCast instance

[NatCast R] : NatCast (SeparationQuotient R)

Full source

instance instNatCast [NatCast R] : NatCast (SeparationQuotient R) where
  natCast n := mk n

Natural Number Casting on the Separation Quotient

Informal description

For any topological space $R$ equipped with a natural number casting operation, the separation quotient $\text{SeparationQuotient}\, R$ inherits a natural number casting operation. This means that for any natural number $n$, the element $n$ in $R$ maps to the corresponding element $n$ in $\text{SeparationQuotient}\, R$ under the quotient map.

SeparationQuotient.mk_natCast theorem

[NatCast R] (n : ℕ) : mk (n : R) = n

Full source

@[simp, norm_cast]
theorem mk_natCast [NatCast R] (n : ℕ) : mk (n : R) = n := rfl

Natural Number Cast Preservation in Separation Quotient Projection

Informal description

For any topological space $R$ with a natural number casting operation, the projection map $\text{mk}$ from $R$ to its separation quotient $\text{SeparationQuotient}\, R$ preserves natural number casts. That is, for any natural number $n$, we have $\text{mk}(n) = n$ in the separation quotient.

SeparationQuotient.mk_ofNat theorem

[NatCast R] (n : ℕ) [n.AtLeastTwo] : mk (ofNat(n) : R) = OfNat.ofNat n

Full source

@[simp]
theorem mk_ofNat [NatCast R] (n : ℕ) [n.AtLeastTwo] :
    mk (ofNat(n) : R) = OfNat.ofNat n :=
  rfl

Preservation of Numerals ≥ 2 in Separation Quotient Projection

Informal description

For any topological space $R$ with a natural number casting operation and any natural number $n \geq 2$, the projection map $\text{mk}$ from $R$ to its separation quotient $\text{SeparationQuotient}\, R$ satisfies $\text{mk}(n) = n$, where $n$ on the right-hand side is interpreted as an element of the separation quotient via the `OfNat` instance.

SeparationQuotient.instIntCast instance

[IntCast R] : IntCast (SeparationQuotient R)

Full source

instance instIntCast [IntCast R] : IntCast (SeparationQuotient R) where
  intCast n := mk n

Integer Casting on Separation Quotient

Informal description

For any topological space $R$ with integer casting operation, the separation quotient of $R$ inherits an integer casting operation.

SeparationQuotient.mk_intCast theorem

[IntCast R] (n : ℤ) : mk (n : R) = n

Full source

@[simp, norm_cast]
theorem mk_intCast [IntCast R] (n : ℤ) : mk (n : R) = n := rfl

Integer Casting Commutes with Separation Quotient Projection

Informal description

For any topological space $R$ with an integer casting operation and any integer $n \in \mathbb{Z}$, the projection map $\mathrm{mk}$ from $R$ to its separation quotient satisfies $\mathrm{mk}(n) = n$, where the left-hand side interprets $n$ as an element of $R$ and the right-hand side interprets $n$ as an element of the separation quotient of $R$.

SeparationQuotient.instNonAssocSemiring instance

[NonAssocSemiring R] [IsTopologicalSemiring R] : NonAssocSemiring (SeparationQuotient R)

Full source

instance instNonAssocSemiring [NonAssocSemiring R] [IsTopologicalSemiring R] :
    NonAssocSemiring (SeparationQuotient R) :=
  surjective_mk.nonAssocSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_natCast

Non-Associative Semiring Structure on the Separation Quotient of a Topological Non-Associative Semiring

Informal description

For any topological space $R$ equipped with a non-associative semiring structure and continuous addition and multiplication operations, the separation quotient $\operatorname{SeparationQuotient} R$ inherits a non-associative semiring structure. The operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonUnitalNonAssocRing instance

[NonUnitalNonAssocRing R] [IsTopologicalRing R] : NonUnitalNonAssocRing (SeparationQuotient R)

Full source

instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
    NonUnitalNonAssocRing (SeparationQuotient R) :=
  surjective_mk.nonUnitalNonAssocRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul

Non-unital Non-associative Ring Structure on the Separation Quotient of a Topological Ring

Informal description

For any topological space $R$ equipped with a non-unital non-associative ring structure and continuous ring operations, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital non-associative ring structure. The operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonUnitalRing instance

[NonUnitalRing R] [IsTopologicalRing R] : NonUnitalRing (SeparationQuotient R)

Full source

instance instNonUnitalRing [NonUnitalRing R] [IsTopologicalRing R] :
    NonUnitalRing (SeparationQuotient R) :=
  surjective_mk.nonUnitalRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul

Non-Unital Ring Structure on the Separation Quotient of a Topological Non-Unital Ring

Informal description

For any topological space $R$ equipped with a non-unital ring structure and continuous ring operations, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital ring structure, where the operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonAssocRing instance

[NonAssocRing R] [IsTopologicalRing R] : NonAssocRing (SeparationQuotient R)

Full source

instance instNonAssocRing [NonAssocRing R] [IsTopologicalRing R] :
    NonAssocRing (SeparationQuotient R) :=
  surjective_mk.nonAssocRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul
    mk_natCast mk_intCast

Non-Associative Ring Structure on the Separation Quotient of a Topological Non-Associative Ring

Informal description

For any topological space $R$ equipped with a non-associative ring structure and continuous ring operations, the separation quotient $\operatorname{SeparationQuotient} R$ inherits a non-associative ring structure. The operations are defined by lifting the original ring operations through the quotient map.

SeparationQuotient.instSemiring instance

[Semiring R] [IsTopologicalSemiring R] : Semiring (SeparationQuotient R)

Full source

instance instSemiring [Semiring R] [IsTopologicalSemiring R] :
    Semiring (SeparationQuotient R) :=
  surjective_mk.semiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_pow mk_natCast

Semiring Structure on the Separation Quotient of a Topological Semiring

Informal description

For any topological semiring $R$ with continuous operations, the separation quotient $\text{SeparationQuotient } R$ inherits a semiring structure, where the operations are defined by lifting the original semiring operations through the quotient map.

SeparationQuotient.instRing instance

[Ring R] [IsTopologicalRing R] : Ring (SeparationQuotient R)

Full source

instance instRing [Ring R] [IsTopologicalRing R] :
    Ring (SeparationQuotient R) :=
  surjective_mk.ring mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow
    mk_natCast mk_intCast

Ring Structure on the Separation Quotient of a Topological Ring

Informal description

For any topological ring $R$ with continuous ring operations, the separation quotient $\operatorname{SeparationQuotient} R$ inherits a ring structure. The operations are defined by lifting the original ring operations through the quotient map.

SeparationQuotient.instNonUnitalNonAssocCommSemiring instance

[NonUnitalNonAssocCommSemiring R] [IsTopologicalSemiring R] : NonUnitalNonAssocCommSemiring (SeparationQuotient R)

Full source

instance instNonUnitalNonAssocCommSemiring [NonUnitalNonAssocCommSemiring R]
    [IsTopologicalSemiring R] :
    NonUnitalNonAssocCommSemiring (SeparationQuotient R) :=
  surjective_mk.nonUnitalNonAssocCommSemiring mk mk_zero mk_add mk_mul mk_smul

Non-Unital Non-Associative Commutative Semiring Structure on Separation Quotient

Informal description

For any topological space $R$ equipped with a continuous non-unital non-associative commutative semiring structure, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital non-associative commutative semiring structure, where the operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instNonUnitalCommSemiring instance

[NonUnitalCommSemiring R] [IsTopologicalSemiring R] : NonUnitalCommSemiring (SeparationQuotient R)

Full source

instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] [IsTopologicalSemiring R] :
    NonUnitalCommSemiring (SeparationQuotient R) :=
  surjective_mk.nonUnitalCommSemiring mk mk_zero mk_add mk_mul mk_smul

Non-Unital Commutative Semiring Structure on the Separation Quotient of a Topological Semiring

Informal description

For any topological space $R$ equipped with a continuous multiplication and addition that forms a non-unital commutative semiring, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital commutative semiring structure. The operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instCommSemiring instance

[CommSemiring R] [IsTopologicalSemiring R] : CommSemiring (SeparationQuotient R)

Full source

instance instCommSemiring [CommSemiring R] [IsTopologicalSemiring R] :
    CommSemiring (SeparationQuotient R) :=
  surjective_mk.commSemiring mk mk_zero mk_one mk_add mk_mul mk_smul mk_pow mk_natCast

Commutative Semiring Structure on the Separation Quotient of a Topological Semiring

Informal description

For any topological space $R$ equipped with a commutative semiring structure and continuous semiring operations, the separation quotient $\operatorname{SeparationQuotient} R$ inherits a commutative semiring structure. The operations are defined by lifting the original operations through the quotient map.

SeparationQuotient.instHasDistribNeg instance

[Mul R] [HasDistribNeg R] [ContinuousMul R] [ContinuousNeg R] : HasDistribNeg (SeparationQuotient R)

Full source

instance instHasDistribNeg [Mul R] [HasDistribNeg R] [ContinuousMul R] [ContinuousNeg R] :
    HasDistribNeg (SeparationQuotient R) :=
  surjective_mk.hasDistribNeg mk mk_neg mk_mul

Distributivity of Negation over Multiplication in the Separation Quotient

Informal description

For any topological space $R$ equipped with a multiplication operation and a negation operation that distributes over multiplication, if both operations are continuous, then the separation quotient $\text{SeparationQuotient } R$ inherits a negation operation that distributes over multiplication.

SeparationQuotient.instNonUnitalNonAssocCommRing instance

[NonUnitalNonAssocCommRing R] [IsTopologicalRing R] : NonUnitalNonAssocCommRing (SeparationQuotient R)

Full source

instance instNonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R] [IsTopologicalRing R] :
    NonUnitalNonAssocCommRing (SeparationQuotient R) :=
  surjective_mk.nonUnitalNonAssocCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul

Non-Unital Non-Associative Commutative Ring Structure on the Separation Quotient

Informal description

For any topological space $R$ equipped with a non-unital non-associative commutative ring structure and continuous ring operations, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital non-associative commutative ring structure.

SeparationQuotient.instNonUnitalCommRing instance

[NonUnitalCommRing R] [IsTopologicalRing R] : NonUnitalCommRing (SeparationQuotient R)

Full source

instance instNonUnitalCommRing [NonUnitalCommRing R] [IsTopologicalRing R] :
    NonUnitalCommRing (SeparationQuotient R) :=
  surjective_mk.nonUnitalCommRing mk mk_zero mk_add mk_mul mk_neg mk_sub mk_smul mk_smul

Non-Unital Commutative Ring Structure on the Separation Quotient

Informal description

For any topological space $R$ equipped with a non-unital commutative ring structure and continuous ring operations, the separation quotient $\text{SeparationQuotient } R$ inherits a non-unital commutative ring structure. The operations on the quotient are defined by lifting the original operations through the quotient map.

SeparationQuotient.instCommRing instance

[CommRing R] [IsTopologicalRing R] : CommRing (SeparationQuotient R)

Full source

instance instCommRing [CommRing R] [IsTopologicalRing R] :
    CommRing (SeparationQuotient R) :=
  surjective_mk.commRing mk mk_zero mk_one mk_add mk_mul mk_neg mk_sub mk_smul mk_smul mk_pow
    mk_natCast mk_intCast

Commutative Ring Structure on the Separation Quotient of a Topological Commutative Ring

Informal description

For any topological space $R$ equipped with a commutative ring structure and continuous ring operations, the separation quotient $\operatorname{SeparationQuotient} R$ inherits a commutative ring structure. The ring operations on the quotient are defined by lifting the original operations through the quotient map.

SeparationQuotient.mkRingHom definition

[NonAssocSemiring R] [IsTopologicalSemiring R] : R →+* SeparationQuotient R

Full source

/-- `SeparationQuotient.mk` as a `RingHom`. -/
@[simps]
def mkRingHom [NonAssocSemiring R] [IsTopologicalSemiring R] : R →+* SeparationQuotient R where
  toFun := mk
  map_one' := mk_one; map_zero' := mk_zero; map_add' := mk_add; map_mul' := mk_mul

Separation quotient projection as a semiring homomorphism

Informal description

The natural projection map from a topological non-associative semiring $R$ to its separation quotient, viewed as a semiring homomorphism. This map preserves the additive and multiplicative structures, sending $1$ to $1$, $0$ to $0$, addition to addition, and multiplication to multiplication.

SeparationQuotient.instDistribSMul instance

[AddZeroClass A] [DistribSMul M A] [ContinuousAdd A] [ContinuousConstSMul M A] : DistribSMul M (SeparationQuotient A)

Full source

instance instDistribSMul [AddZeroClass A] [DistribSMul M A]
    [ContinuousAdd A] [ContinuousConstSMul M A] :
    DistribSMul M (SeparationQuotient A) :=
  surjective_mk.distribSMul mkAddMonoidHom mk_smul

Distributive Scalar Multiplication on the Separation Quotient

Informal description

For any topological space $A$ with an additive zero class structure and a distributive scalar multiplication action by $M$, if addition is continuous in $A$ and scalar multiplication is continuous in the second variable, then the separation quotient $\text{SeparationQuotient } A$ inherits a distributive scalar multiplication structure from $A$.

SeparationQuotient.instDistribMulAction instance

 [Monoid M] [AddMonoid A] [DistribMulAction M A] [ContinuousAdd A] [ContinuousConstSMul M A] :
  DistribMulAction M (SeparationQuotient A)

Full source

instance instDistribMulAction [Monoid M] [AddMonoid A] [DistribMulAction M A]
    [ContinuousAdd A] [ContinuousConstSMul M A] :
    DistribMulAction M (SeparationQuotient A) :=
  surjective_mk.distribMulAction mkAddMonoidHom mk_smul

Distributive Multiplicative Action on the Separation Quotient

Informal description

For any topological space $A$ with an additive monoid structure and a distributive multiplicative action by a monoid $M$, if addition in $A$ is continuous and scalar multiplication by each fixed element of $M$ is continuous, then the separation quotient $\text{SeparationQuotient } A$ inherits a distributive multiplicative action structure from $A$.

SeparationQuotient.instMulDistribMulAction instance

 [Monoid M] [Monoid A] [MulDistribMulAction M A] [ContinuousMul A] [ContinuousConstSMul M A] :
  MulDistribMulAction M (SeparationQuotient A)

Full source

instance instMulDistribMulAction [Monoid M] [Monoid A] [MulDistribMulAction M A]
    [ContinuousMul A] [ContinuousConstSMul M A] :
    MulDistribMulAction M (SeparationQuotient A) :=
  surjective_mk.mulDistribMulAction mkMonoidHom mk_smul

Multiplicative Distributive Action on the Separation Quotient of a Topological Monoid

Informal description

For any topological monoid $A$ with a multiplicative distributive action by a monoid $M$, if the multiplication in $A$ is continuous and the scalar multiplication by each fixed element of $M$ is continuous, then the separation quotient $\text{SeparationQuotient } A$ inherits a multiplicative distributive action structure from $A$.

SeparationQuotient.instModule instance

: Module R (SeparationQuotient M)

Full source

instance instModule : Module R (SeparationQuotient M) :=
  surjective_mk.module R mkAddMonoidHom mk_smul

Module Structure on the Separation Quotient

Informal description

For any topological space $M$ with a module structure over a ring $R$ where scalar multiplication is continuous in the second variable, the separation quotient $\text{SeparationQuotient } M$ inherits a canonical module structure over $R$.

SeparationQuotient.mkCLM definition

: M →L[R] SeparationQuotient M

Full source

/-- `SeparationQuotient.mk` as a continuous linear map. -/
@[simps]
def mkCLM : M →L[R] SeparationQuotient M where
  toFun := mk
  map_add' := mk_add
  map_smul' := mk_smul

Continuous linear projection to the separation quotient

Informal description

The natural projection map $\operatorname{mk} : M \to \operatorname{SeparationQuotient} M$ as a continuous linear map, where $\operatorname{SeparationQuotient} M$ is the quotient space obtained by identifying inseparable points in the topological space $M$. This map preserves addition and scalar multiplication, and is continuous with respect to the inherited topology on the separation quotient.

SeparationQuotient.liftCLM definition

{σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) : SeparationQuotient M →SL[σ] N

Full source

/-- The lift (as a continuous linear map) of `f` with `f x = f y` for `Inseparable x y`. -/
@[simps]
noncomputable def liftCLM {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) :
    SeparationQuotientSeparationQuotient M →SL[σ] N where
  toFun := SeparationQuotient.lift f hf
  map_add' := Quotient.ind₂ <| map_add f
  map_smul' {r} := Quotient.ind <| map_smulₛₗ f r

Lifting of a continuous linear map to the separation quotient

Informal description

Given a continuous linear map $ f : M \to N $ between topological modules over rings $ R $ and $ S $ with a ring homomorphism $ \sigma : R \to S $, and assuming $ f $ respects the inseparable relation (i.e., $ f(x) = f(y) $ whenever $ x $ and $ y $ are inseparable in $ M $), the function `SeparationQuotient.liftCLM` lifts $ f $ to a continuous linear map from the separation quotient $ \text{SeparationQuotient}\, M $ to $ N $. This lifted map preserves both the additive and scalar multiplication structures.

SeparationQuotient.liftCLM_mk theorem

{σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y) (x : M) : liftCLM f hf (mk x) = f x

Full source

@[simp]
theorem liftCLM_mk {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ x y, Inseparable x y → f x = f y)
    (x : M) : liftCLM f hf (mk x) = f x := rfl

Commutativity of Lifting Continuous Linear Maps through Separation Quotient

Informal description

Let $M$ and $N$ be topological modules over rings $R$ and $S$ respectively, with a ring homomorphism $\sigma : R \to S$. Given a continuous linear map $f : M \to N$ that respects inseparability (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $M$), then for any $x \in M$, the lifted map $\operatorname{liftCLM}(f, hf)$ applied to the projection $\operatorname{mk}(x)$ equals $f(x)$. In other words, the following diagram commutes: $$\operatorname{liftCLM}(f, hf)(\operatorname{mk}(x)) = f(x).$$

SeparationQuotient.instAlgebra instance

: Algebra R (SeparationQuotient A)

Full source

instance instAlgebra : Algebra R (SeparationQuotient A) where
  algebraMap := mkRingHom.comp (algebraMap R A)
  commutes' r := Quotient.ind fun a => congrArg _ <| Algebra.commutes r a
  smul_def' r := Quotient.ind fun a => congrArg _ <| Algebra.smul_def r a

Algebra Structure on the Separation Quotient of a Topological Algebra

Informal description

For any topological algebra $A$ over a commutative ring $R$ with continuous operations, the separation quotient $\text{SeparationQuotient } A$ inherits an algebra structure over $R$. The algebra operations are defined by lifting the original algebra operations through the quotient map.

SeparationQuotient.mk_algebraMap theorem

(r : R) : mk (algebraMap R A r) = algebraMap R (SeparationQuotient A) r

Full source

@[simp]
theorem mk_algebraMap (r : R) : mk (algebraMap R A r) = algebraMap R (SeparationQuotient A) r :=
  rfl

Compatibility of Algebra Map with Separation Quotient Projection

Informal description

For any topological algebra $A$ over a commutative ring $R$ with continuous operations, and for any element $r \in R$, the image of the algebra map $\text{algebraMap}_R^A(r)$ under the separation quotient projection $\text{mk}$ equals the algebra map $\text{algebraMap}_R^{\text{SeparationQuotient } A}(r)$. In other words, the following diagram commutes: $$\text{mk}(\text{algebraMap}_R^A(r)) = \text{algebraMap}_R^{\text{SeparationQuotient } A}(r).$$