Algebraic operations on `SeparationQuotient` #

In this file we define algebraic operations (multiplication, addition etc) on the separation quotient of a topological space with corresponding operation, provided that the original operation is continuous.

We also prove continuity of these operations and show that they satisfy the same kind of laws (Monoid etc) as the original ones.

Finally, we construct a section of the quotient map which is a continuous linear map SeparationQuotient E →L[K] E.

source

instance SeparationQuotient.instSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] :

SMul M (SeparationQuotient X)

Equations

source

instance SeparationQuotient.instVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] :

VAdd M (SeparationQuotient X)

Equations

source

@[simp]

theorem SeparationQuotient.mk_smul {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] (c : M) (x : X) :

mk (c • x) = c • mk x

source

@[simp]

theorem SeparationQuotient.mk_vadd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] (c : M) (x : X) :

mk (c +ᵥ x) = c +ᵥ mk x

source

instance SeparationQuotient.instContinuousConstSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] :

ContinuousConstSMul M (SeparationQuotient X)

source

instance SeparationQuotient.instContinuousConstVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] :

ContinuousConstVAdd M (SeparationQuotient X)

source

instance SeparationQuotient.instIsPretransitiveSMul {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] [MulAction.IsPretransitive M X] :

MulAction.IsPretransitive M (SeparationQuotient X)

source

instance SeparationQuotient.instIsPretransitiveVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] [AddAction.IsPretransitive M X] :

AddAction.IsPretransitive M (SeparationQuotient X)

source

instance SeparationQuotient.instIsCentralScalar {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] :

IsCentralScalar M (SeparationQuotient X)

source

instance SeparationQuotient.instIsCentralVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] :

IsCentralVAdd M (SeparationQuotient X)

source

instance SeparationQuotient.instSMulCommClass {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] {N : Type u_3} [SMul N X] [ContinuousConstSMul N X] [SMulCommClass M N X] :

SMulCommClass M N (SeparationQuotient X)

source

instance SeparationQuotient.instVAddCommClass {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] {N : Type u_3} [VAdd N X] [ContinuousConstVAdd N X] [VAddCommClass M N X] :

VAddCommClass M N (SeparationQuotient X)

source

instance SeparationQuotient.instIsScalarTower {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] {N : Type u_3} [SMul N X] [SMul M N] [ContinuousConstSMul N X] [IsScalarTower M N X] :

IsScalarTower M N (SeparationQuotient X)

source

instance SeparationQuotient.instVAddAssocClass {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] {N : Type u_3} [VAdd N X] [VAdd M N] [ContinuousConstVAdd N X] [VAddAssocClass M N X] :

VAddAssocClass M N (SeparationQuotient X)

source

instance SeparationQuotient.instContinuousSMul {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace M] [TopologicalSpace X] [ContinuousSMul M X] :

ContinuousSMul M (SeparationQuotient X)

source

instance SeparationQuotient.instSMulZeroClass {M : Type u_1} {X : Type u_2} [Zero X] [SMulZeroClass M X] [TopologicalSpace X] [ContinuousConstSMul M X] :

SMulZeroClass M (SeparationQuotient X)

Equations

source

instance SeparationQuotient.instMulAction {M : Type u_1} {X : Type u_2} [Monoid M] [MulAction M X] [TopologicalSpace X] [ContinuousConstSMul M X] :

MulAction M (SeparationQuotient X)

Equations

source

instance SeparationQuotient.instAddAction {M : Type u_1} {X : Type u_2} [AddMonoid M] [AddAction M X] [TopologicalSpace X] [ContinuousConstVAdd M X] :

AddAction M (SeparationQuotient X)

Equations

source

instance SeparationQuotient.instMul {M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] :

Mul (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAdd {M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] :

Add (SeparationQuotient M)

Equations

source

@[simp]

theorem SeparationQuotient.mk_mul {M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] (a b : M) :

mk (a * b) = mk a * mk b

source

@[simp]

theorem SeparationQuotient.mk_add {M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] (a b : M) :

mk (a + b) = mk a + mk b

source

instance SeparationQuotient.instContinuousMul {M : Type u_1} [TopologicalSpace M] [Mul M] [ContinuousMul M] :

ContinuousMul (SeparationQuotient M)

source

instance SeparationQuotient.instContinuousAdd {M : Type u_1} [TopologicalSpace M] [Add M] [ContinuousAdd M] :

ContinuousAdd (SeparationQuotient M)

source

instance SeparationQuotient.instCommMagma {M : Type u_1} [TopologicalSpace M] [CommMagma M] [ContinuousMul M] :

CommMagma (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddCommMagma {M : Type u_1} [TopologicalSpace M] [AddCommMagma M] [ContinuousAdd M] :

AddCommMagma (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instSemigroup {M : Type u_1} [TopologicalSpace M] [Semigroup M] [ContinuousMul M] :

Semigroup (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddSemigroup {M : Type u_1} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] :

AddSemigroup (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instCommSemigroup {M : Type u_1} [TopologicalSpace M] [CommSemigroup M] [ContinuousMul M] :

CommSemigroup (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddCommSemigroup {M : Type u_1} [TopologicalSpace M] [AddCommSemigroup M] [ContinuousAdd M] :

AddCommSemigroup (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instMulOneClass {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] :

MulOneClass (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddZeroClass {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] :

AddZeroClass (SeparationQuotient M)

Equations

source

def SeparationQuotient.mkMonoidHom {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] :

M →* SeparationQuotient M

SeparationQuotient.mk as a MonoidHom.

Equations

Instances For

source

def SeparationQuotient.mkAddMonoidHom {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] :

M →+ SeparationQuotient M

SeparationQuotient.mk as an AddMonoidHom.

Equations

Instances For

source

@[simp]

theorem SeparationQuotient.mkMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] (a✝ : M) :

mkMonoidHom a✝ = mk a✝

source

@[simp]

theorem SeparationQuotient.mkAddMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] (a✝ : M) :

mkAddMonoidHom a✝ = mk a✝

source

instance SeparationQuotient.instNSmul {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] :

SMul ℕ (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instPow {M : Type u_1} [TopologicalSpace M] [Monoid M] [ContinuousMul M] :

Pow (SeparationQuotient M) ℕ

Equations

source

@[simp]

theorem SeparationQuotient.mk_pow {M : Type u_1} [TopologicalSpace M] [Monoid M] [ContinuousMul M] (x : M) (n : ℕ) :

mk (x ^ n) = mk x ^ n

source

theorem SeparationQuotient.mk_nsmul {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (x : M) (n : ℕ) :

mk (n • x) = n • mk x

source

instance SeparationQuotient.instMonoid {M : Type u_1} [TopologicalSpace M] [Monoid M] [ContinuousMul M] :

Monoid (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddMonoid {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] :

AddMonoid (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instCommMonoid {M : Type u_1} [TopologicalSpace M] [CommMonoid M] [ContinuousMul M] :

CommMonoid (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instAddCommMonoid {M : Type u_1} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] :

AddCommMonoid (SeparationQuotient M)

Equations

source

instance SeparationQuotient.instInv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] :

Inv (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instNeg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] :

Neg (SeparationQuotient G)

Equations

source

@[simp]

theorem SeparationQuotient.mk_inv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] (x : G) :

mk x⁻¹ = (mk x)⁻¹

source

@[simp]

theorem SeparationQuotient.mk_neg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] (x : G) :

mk (-x) = -mk x

source

instance SeparationQuotient.instContinuousInv {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] :

ContinuousInv (SeparationQuotient G)

source

instance SeparationQuotient.instContinuousNeg {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] :

ContinuousNeg (SeparationQuotient G)

source

instance SeparationQuotient.instInvolutiveInv {G : Type u_1} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :

InvolutiveInv (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instInvolutiveNeg {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] :

InvolutiveNeg (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instInvOneClass {G : Type u_1} [TopologicalSpace G] [InvOneClass G] [ContinuousInv G] :

InvOneClass (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instNegZeroClass {G : Type u_1} [TopologicalSpace G] [NegZeroClass G] [ContinuousNeg G] :

NegZeroClass (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instDiv {G : Type u_1} [TopologicalSpace G] [Div G] [ContinuousDiv G] :

Div (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instSub {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] :

Sub (SeparationQuotient G)

Equations

source

@[simp]

theorem SeparationQuotient.mk_div {G : Type u_1} [TopologicalSpace G] [Div G] [ContinuousDiv G] (x y : G) :

mk (x / y) = mk x / mk y

source

@[simp]

theorem SeparationQuotient.mk_sub {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] (x y : G) :

mk (x - y) = mk x - mk y

source

instance SeparationQuotient.instContinuousDiv {G : Type u_1} [TopologicalSpace G] [Div G] [ContinuousDiv G] :

ContinuousDiv (SeparationQuotient G)

source

instance SeparationQuotient.instContinuousSub {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] :

ContinuousSub (SeparationQuotient G)

source

instance SeparationQuotient.instZSMul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] :

SMul ℤ (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instZPow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

Pow (SeparationQuotient G) ℤ

Equations

source

@[simp]

theorem SeparationQuotient.mk_zpow {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (x : G) (n : ℤ) :

mk (x ^ n) = mk x ^ n

source

theorem SeparationQuotient.mk_zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (x : G) (n : ℤ) :

mk (n • x) = n • mk x

source

instance SeparationQuotient.instGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

Group (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] :

AddGroup (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instCommGroup {G : Type u_1} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] :

CommGroup (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instAddCommGroup {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] :

AddCommGroup (SeparationQuotient G)

Equations

source

instance SeparationQuotient.instIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :

IsTopologicalGroup (SeparationQuotient G)

source

instance SeparationQuotient.instIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] :

IsTopologicalAddGroup (SeparationQuotient G)

source

instance SeparationQuotient.instIsUniformGroup {G : Type u_1} [Group G] [UniformSpace G] [IsUniformGroup G] :

IsUniformGroup (SeparationQuotient G)

source

instance SeparationQuotient.instIsUniformAddGroup {G : Type u_1} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] :

IsUniformAddGroup (SeparationQuotient G)

source

@[deprecated SeparationQuotient.instIsUniformAddGroup (since := "2025-03-31")]

theorem SeparationQuotient.instUniformAddGroup {G : Type u_1} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] :

IsUniformAddGroup (SeparationQuotient G)

Alias of SeparationQuotient.instIsUniformAddGroup.

source

@[deprecated SeparationQuotient.instIsUniformGroup (since := "2025-03-31")]

theorem SeparationQuotient.instUniformGroup {G : Type u_1} [Group G] [UniformSpace G] [IsUniformGroup G] :

IsUniformGroup (SeparationQuotient G)

Alias of SeparationQuotient.instIsUniformGroup.

source

instance SeparationQuotient.instMulZeroClass {M₀ : Type u_1} [TopologicalSpace M₀] [MulZeroClass M₀] [ContinuousMul M₀] :

MulZeroClass (SeparationQuotient M₀)

Equations

source

instance SeparationQuotient.instSemigroupWithZero {M₀ : Type u_1} [TopologicalSpace M₀] [SemigroupWithZero M₀] [ContinuousMul M₀] :

SemigroupWithZero (SeparationQuotient M₀)

Equations

source

instance SeparationQuotient.instMulZeroOneClass {M₀ : Type u_1} [TopologicalSpace M₀] [MulZeroOneClass M₀] [ContinuousMul M₀] :

MulZeroOneClass (SeparationQuotient M₀)

Equations

source

instance SeparationQuotient.instMonoidWithZero {M₀ : Type u_1} [TopologicalSpace M₀] [MonoidWithZero M₀] [ContinuousMul M₀] :

MonoidWithZero (SeparationQuotient M₀)

Equations

source

instance SeparationQuotient.instCommMonoidWithZero {M₀ : Type u_1} [TopologicalSpace M₀] [CommMonoidWithZero M₀] [ContinuousMul M₀] :

CommMonoidWithZero (SeparationQuotient M₀)

Equations

source

instance SeparationQuotient.instDistrib {R : Type u_1} [TopologicalSpace R] [Distrib R] [ContinuousMul R] [ContinuousAdd R] :

Distrib (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instLeftDistribClass {R : Type u_1} [TopologicalSpace R] [Mul R] [Add R] [LeftDistribClass R] [ContinuousMul R] [ContinuousAdd R] :

LeftDistribClass (SeparationQuotient R)

source

instance SeparationQuotient.instRightDistribClass {R : Type u_1} [TopologicalSpace R] [Mul R] [Add R] [RightDistribClass R] [ContinuousMul R] [ContinuousAdd R] :

RightDistribClass (SeparationQuotient R)

source

instance SeparationQuotient.instNonUnitalnonAssocSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] :

NonUnitalNonAssocSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] :

NonUnitalSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNatCast {R : Type u_1} [TopologicalSpace R] [NatCast R] :

NatCast (SeparationQuotient R)

Equations

source

@[simp]

theorem SeparationQuotient.mk_natCast {R : Type u_1} [TopologicalSpace R] [NatCast R] (n : ℕ) :

mk ↑n = ↑n

source

@[simp]

theorem SeparationQuotient.mk_ofNat {R : Type u_1} [TopologicalSpace R] [NatCast R] (n : ℕ) [n.AtLeastTwo] :

mk (OfNat.ofNat n) = OfNat.ofNat n

source

instance SeparationQuotient.instIntCast {R : Type u_1} [TopologicalSpace R] [IntCast R] :

IntCast (SeparationQuotient R)

Equations

source

@[simp]

theorem SeparationQuotient.mk_intCast {R : Type u_1} [TopologicalSpace R] [IntCast R] (n : ℤ) :

mk ↑n = ↑n

source

instance SeparationQuotient.instNonAssocSemiring {R : Type u_1} [TopologicalSpace R] [NonAssocSemiring R] [IsTopologicalSemiring R] :

NonAssocSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalNonAssocRing {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [IsTopologicalRing R] :

NonUnitalNonAssocRing (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalRing {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] :

NonUnitalRing (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonAssocRing {R : Type u_1} [TopologicalSpace R] [NonAssocRing R] [IsTopologicalRing R] :

NonAssocRing (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instSemiring {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] :

Semiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instRing {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] :

Ring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalNonAssocCommSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocCommSemiring R] [IsTopologicalSemiring R] :

NonUnitalNonAssocCommSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalCommSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalCommSemiring R] [IsTopologicalSemiring R] :

NonUnitalCommSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instCommSemiring {R : Type u_1} [TopologicalSpace R] [CommSemiring R] [IsTopologicalSemiring R] :

CommSemiring (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instHasDistribNeg {R : Type u_1} [TopologicalSpace R] [Mul R] [HasDistribNeg R] [ContinuousMul R] [ContinuousNeg R] :

HasDistribNeg (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalNonAssocCommRing {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocCommRing R] [IsTopologicalRing R] :

NonUnitalNonAssocCommRing (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instNonUnitalCommRing {R : Type u_1} [TopologicalSpace R] [NonUnitalCommRing R] [IsTopologicalRing R] :

NonUnitalCommRing (SeparationQuotient R)

Equations

source

instance SeparationQuotient.instCommRing {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] :

CommRing (SeparationQuotient R)

Equations

source

def SeparationQuotient.mkRingHom {R : Type u_1} [TopologicalSpace R] [NonAssocSemiring R] [IsTopologicalSemiring R] :

R →+* SeparationQuotient R

SeparationQuotient.mk as a RingHom.

Equations

Instances For

source

@[simp]

theorem SeparationQuotient.mkRingHom_apply {R : Type u_1} [TopologicalSpace R] [NonAssocSemiring R] [IsTopologicalSemiring R] (a✝ : R) :

mkRingHom a✝ = mk a✝

source

instance SeparationQuotient.instDistribSMul {M : Type u_1} {A : Type u_2} [TopologicalSpace A] [AddZeroClass A] [DistribSMul M A] [ContinuousAdd A] [ContinuousConstSMul M A] :

DistribSMul M (SeparationQuotient A)

Equations

source

instance SeparationQuotient.instDistribMulAction {M : Type u_1} {A : Type u_2} [TopologicalSpace A] [Monoid M] [AddMonoid A] [DistribMulAction M A] [ContinuousAdd A] [ContinuousConstSMul M A] :

DistribMulAction M (SeparationQuotient A)

Equations

source

instance SeparationQuotient.instMulDistribMulAction {M : Type u_1} {A : Type u_2} [TopologicalSpace A] [Monoid M] [Monoid A] [MulDistribMulAction M A] [ContinuousMul A] [ContinuousConstSMul M A] :

MulDistribMulAction M (SeparationQuotient A)

Equations

source

instance SeparationQuotient.instModule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] :

Module R (SeparationQuotient M)

Equations

source

def SeparationQuotient.mkCLM (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] :

M →L[R] SeparationQuotient M

SeparationQuotient.mk as a continuous linear map.

Equations

Instances For

source

@[simp]

theorem SeparationQuotient.mkCLM_apply (R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (a✝ : M) :

(mkCLM R M) a✝ = mk a✝

source

noncomputable def SeparationQuotient.liftCLM {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] [Semiring S] [AddCommMonoid N] [Module S N] [TopologicalSpace N] {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) :

SeparationQuotient M →SL[σ] N

The lift (as a continuous linear map) of f with f x = f y for Inseparable x y.

Equations

Instances For

source

@[simp]

theorem SeparationQuotient.liftCLM_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] [Semiring S] [AddCommMonoid N] [Module S N] [TopologicalSpace N] {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (a✝ : SeparationQuotient M) :

(liftCLM f hf) a✝ = lift (⇑f) hf a✝

source

@[simp]

theorem SeparationQuotient.liftCLM_mk {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] [Semiring S] [AddCommMonoid N] [Module S N] [TopologicalSpace N] {σ : R →+* S} (f : M →SL[σ] N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (x : M) :

(liftCLM f hf) (mk x) = f x

source

instance SeparationQuotient.instAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] :

Algebra R (SeparationQuotient A)

Equations

source

@[simp]

theorem SeparationQuotient.mk_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalSemiring A] [ContinuousConstSMul R A] (r : R) :

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

Documentation

Mathlib.Topology.Algebra.SeparationQuotient.Basic

Algebraic operations on `SeparationQuotient` #

Algebraic operations on SeparationQuotient #

Algebraic operations on `SeparationQuotient` #