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.

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

Equations

• SeparationQuotient.instVAdd = { vadd := fun (c : M) => Quotient.map' (fun (x : X) => c +ᵥ x) ⋯ }

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

Equations

• SeparationQuotient.instSMul = { smul := fun (c : M) => Quotient.map' (fun (x : X) => c • x) ⋯ }

@[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) : SeparationQuotient.mk (c +ᵥ x) = c +ᵥ SeparationQuotient.mk x

@[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) : SeparationQuotient.mk (c • x) = c • SeparationQuotient.mk x

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

• SeparationQuotient.instSMulZeroClass = { toFun := SeparationQuotient.mk, map_zero' := ⋯ }.smulZeroClass ⋯

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

• SeparationQuotient.instAddAction = Function.Surjective.addAction SeparationQuotient.mk ⋯ ⋯

theorem SeparationQuotient.instAddAction.proof_1 {M : Type u_2} {X : Type u_1} [AddMonoid M] [AddAction M X] [TopologicalSpace X] [ContinuousConstVAdd M X] (c : M) (x : X) : SeparationQuotient.mk (c +ᵥ x) = c +ᵥ SeparationQuotient.mk x

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

• SeparationQuotient.instMulAction = Function.Surjective.mulAction SeparationQuotient.mk ⋯ ⋯

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

Equations

• SeparationQuotient.instAdd = { add := Quotient.map₂' (fun (x1 x2 : M) => x1 + x2) ⋯ }

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

Equations

• SeparationQuotient.instMul = { mul := Quotient.map₂' (fun (x1 x2 : M) => x1 * x2) ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem SeparationQuotient.instAddCommMagma.proof_1 {M : Type u_1} [TopologicalSpace M] [AddCommMagma M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

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

Equations

• SeparationQuotient.instAddCommMagma = Function.Surjective.addCommMagma SeparationQuotient.mk ⋯ ⋯

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

Equations

• SeparationQuotient.instCommMagma = Function.Surjective.commMagma SeparationQuotient.mk ⋯ ⋯

theorem SeparationQuotient.instAddSemigroup.proof_1 {M : Type u_1} [TopologicalSpace M] [AddSemigroup M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

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

Equations

• SeparationQuotient.instAddSemigroup = Function.Surjective.addSemigroup SeparationQuotient.mk ⋯ ⋯

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

Equations

• SeparationQuotient.instSemigroup = Function.Surjective.semigroup SeparationQuotient.mk ⋯ ⋯

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

Equations

• SeparationQuotient.instAddCommSemigroup = Function.Surjective.addCommSemigroup SeparationQuotient.mk ⋯ ⋯

theorem SeparationQuotient.instAddCommSemigroup.proof_1 {M : Type u_1} [TopologicalSpace M] [AddCommSemigroup M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

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

Equations

• SeparationQuotient.instCommSemigroup = Function.Surjective.commSemigroup SeparationQuotient.mk ⋯ ⋯

theorem SeparationQuotient.instAddZeroClass.proof_2 {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

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

Equations

• SeparationQuotient.instAddZeroClass = Function.Surjective.addZeroClass SeparationQuotient.mk ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddZeroClass.proof_1 {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] : SeparationQuotient.mk 0 = 0

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

Equations

• SeparationQuotient.instMulOneClass = Function.Surjective.mulOneClass SeparationQuotient.mk ⋯ ⋯ ⋯

theorem SeparationQuotient.mkAddMonoidHom.proof_2 {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

theorem SeparationQuotient.mkAddMonoidHom.proof_1 {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] : SeparationQuotient.mk 0 = 0

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

SeparationQuotient.mk as an AddMonoidHom.

Equations

• SeparationQuotient.mkAddMonoidHom = { toFun := SeparationQuotient.mk, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SeparationQuotient.mkAddMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [AddZeroClass M] [ContinuousAdd M] : ∀ (a : M), SeparationQuotient.mkAddMonoidHom a = SeparationQuotient.mk a

@[simp]

theorem SeparationQuotient.mkMonoidHom_apply {M : Type u_1} [TopologicalSpace M] [MulOneClass M] [ContinuousMul M] : ∀ (a : M), SeparationQuotient.mkMonoidHom a = SeparationQuotient.mk a

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

SeparationQuotient.mk as a MonoidHom.

Equations

• SeparationQuotient.mkMonoidHom = { toFun := SeparationQuotient.mk, map_one' := ⋯, map_mul' := ⋯ }

instance SeparationQuotient.instNSmul {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] : SMul ℕ (SeparationQuotient M)

Equations

• SeparationQuotient.instNSmul = inferInstance

instance SeparationQuotient.instPow {M : Type u_1} [TopologicalSpace M] [Monoid M] [ContinuousMul M] : Pow (SeparationQuotient M) ℕ

Equations

• SeparationQuotient.instPow = { pow := fun (x : SeparationQuotient M) (n : ℕ) => Quotient.map' (fun (x : M) => x ^ n) ⋯ x }

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

@[simp]

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

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

Equations

• SeparationQuotient.instAddMonoid = Function.Surjective.addMonoid SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddMonoid.proof_2 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

theorem SeparationQuotient.instAddMonoid.proof_1 {M : Type u_1} [TopologicalSpace M] [AddMonoid M] : SeparationQuotient.mk 0 = 0

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

Equations

• SeparationQuotient.instMonoid = Function.Surjective.monoid SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddCommMonoid.proof_2 {M : Type u_1} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] (a : M) (b : M) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

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

Equations

• SeparationQuotient.instAddCommMonoid = Function.Surjective.addCommMonoid SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddCommMonoid.proof_1 {M : Type u_1} [TopologicalSpace M] [AddCommMonoid M] : SeparationQuotient.mk 0 = 0

theorem SeparationQuotient.instAddCommMonoid.proof_3 {M : Type u_1} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] (x : M) (n : ℕ) : SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x

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

Equations

• SeparationQuotient.instCommMonoid = Function.Surjective.commMonoid SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instNeg = { neg := Quotient.map' (fun (x : G) => -x) ⋯ }

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

Equations

• SeparationQuotient.instInv = { inv := Quotient.map' (fun (x : G) => x⁻¹) ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• SeparationQuotient.instInvolutiveNeg = Function.Surjective.involutiveNeg SeparationQuotient.mk ⋯ ⋯

theorem SeparationQuotient.instInvolutiveNeg.proof_1 {G : Type u_1} [TopologicalSpace G] [InvolutiveNeg G] [ContinuousNeg G] (x : G) : SeparationQuotient.mk (-x) = -SeparationQuotient.mk x

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

Equations

• SeparationQuotient.instInvolutiveInv = Function.Surjective.involutiveInv SeparationQuotient.mk ⋯ ⋯

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

Equations

• SeparationQuotient.instNegZeroClass = NegZeroClass.mk ⋯

theorem SeparationQuotient.instNegZeroClass.proof_1 {G : Type u_1} [TopologicalSpace G] [NegZeroClass G] : SeparationQuotient.mk ((fun (x : G) => -x) 0) = SeparationQuotient.mk 0

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

Equations

• SeparationQuotient.instInvOneClass = InvOneClass.mk ⋯

theorem SeparationQuotient.instSub.proof_1 {G : Type u_1} [TopologicalSpace G] [Sub G] [ContinuousSub G] : ∀ (x x_1 : G), Setoid.r x x_1 → ∀ (x_2 x_3 : G), Setoid.r x_2 x_3 → Inseparable ((x, x_2).1 - (x, x_2).2) ((x_1, x_3).1 - (x_1, x_3).2)

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

Equations

• SeparationQuotient.instSub = { sub := Quotient.map₂' (fun (x1 x2 : G) => x1 - x2) ⋯ }

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

Equations

• SeparationQuotient.instDiv = { div := Quotient.map₂' (fun (x1 x2 : G) => x1 / x2) ⋯ }

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance SeparationQuotient.instZSMul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : SMul ℤ (SeparationQuotient G)

Equations

• SeparationQuotient.instZSMul = inferInstance

instance SeparationQuotient.instZPow {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] : Pow (SeparationQuotient G) ℤ

Equations

• SeparationQuotient.instZPow = { pow := fun (x : SeparationQuotient G) (n : ℤ) => Quotient.map' (fun (x : G) => x ^ n) ⋯ x }

theorem SeparationQuotient.mk_zsmul {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (n : ℤ) : SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x

@[simp]

theorem SeparationQuotient.mk_zpow {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (x : G) (n : ℤ) : SeparationQuotient.mk (x ^ n) = SeparationQuotient.mk x ^ n

instance SeparationQuotient.instAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] : AddGroup (SeparationQuotient G)

Equations

• SeparationQuotient.instAddGroup = Function.Surjective.addGroup SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddGroup.proof_2 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (a : G) (b : G) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

theorem SeparationQuotient.instAddGroup.proof_3 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) : SeparationQuotient.mk (-x) = -SeparationQuotient.mk x

theorem SeparationQuotient.instAddGroup.proof_1 {G : Type u_1} [TopologicalSpace G] [AddGroup G] : SeparationQuotient.mk 0 = 0

theorem SeparationQuotient.instAddGroup.proof_5 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (n : ℕ) : SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x

theorem SeparationQuotient.instAddGroup.proof_4 {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (x : G) (y : G) : SeparationQuotient.mk (x - y) = SeparationQuotient.mk x - SeparationQuotient.mk y

instance SeparationQuotient.instGroup {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] : Group (SeparationQuotient G)

Equations

• SeparationQuotient.instGroup = Function.Surjective.group SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem SeparationQuotient.instAddCommGroup.proof_9 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (x : G) (n : ℤ) : SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x

theorem SeparationQuotient.instAddCommGroup.proof_4 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] : SeparationQuotient.mk 0 = 0

theorem SeparationQuotient.instAddCommGroup.proof_2 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] : ContinuousNeg G

theorem SeparationQuotient.instAddCommGroup.proof_6 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (x : G) : SeparationQuotient.mk (-x) = -SeparationQuotient.mk x

theorem SeparationQuotient.instAddCommGroup.proof_3 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] : ContinuousSub G

theorem SeparationQuotient.instAddCommGroup.proof_7 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (x : G) (y : G) : SeparationQuotient.mk (x - y) = SeparationQuotient.mk x - SeparationQuotient.mk y

theorem SeparationQuotient.instAddCommGroup.proof_1 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] : ContinuousAdd G

theorem SeparationQuotient.instAddCommGroup.proof_5 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (a : G) (b : G) : SeparationQuotient.mk (a + b) = SeparationQuotient.mk a + SeparationQuotient.mk b

theorem SeparationQuotient.instAddCommGroup.proof_8 {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (x : G) (n : ℕ) : SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x

instance SeparationQuotient.instAddCommGroup {G : Type u_1} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] : AddCommGroup (SeparationQuotient G)

Equations

• SeparationQuotient.instAddCommGroup = Function.Surjective.addCommGroup SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instCommGroup {G : Type u_1} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] : CommGroup (SeparationQuotient G)

Equations

• SeparationQuotient.instCommGroup = Function.Surjective.commGroup SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instMulZeroClass = Function.Surjective.mulZeroClass SeparationQuotient.mk ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instSemigroupWithZero = Function.Surjective.semigroupWithZero SeparationQuotient.mk ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instMulZeroOneClass = Function.Surjective.mulZeroOneClass SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instMonoidWithZero = Function.Surjective.monoidWithZero SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instCommMonoidWithZero = Function.Surjective.commMonoidWithZero SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instDistrib = Function.Surjective.distrib SeparationQuotient.mk ⋯ ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance SeparationQuotient.instNonUnitalnonAssocSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [TopologicalSemiring R] : NonUnitalNonAssocSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalnonAssocSemiring = Function.Surjective.nonUnitalNonAssocSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [TopologicalSemiring R] : NonUnitalSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalSemiring = Function.Surjective.nonUnitalSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instNatCast = { natCast := fun (n : ℕ) => SeparationQuotient.mk ↑n }

@[simp]

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

@[simp]

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

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

Equations

• SeparationQuotient.instIntCast = { intCast := fun (n : ℤ) => SeparationQuotient.mk ↑n }

@[simp]

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

instance SeparationQuotient.instNonAssocSemiring {R : Type u_1} [TopologicalSpace R] [NonAssocSemiring R] [TopologicalSemiring R] : NonAssocSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instNonAssocSemiring = Function.Surjective.nonAssocSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalNonAssocRing {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [TopologicalRing R] : NonUnitalNonAssocRing (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalNonAssocRing = Function.Surjective.nonUnitalNonAssocRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalRing {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [TopologicalRing R] : NonUnitalRing (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalRing = Function.Surjective.nonUnitalRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonAssocRing {R : Type u_1} [TopologicalSpace R] [NonAssocRing R] [TopologicalRing R] : NonAssocRing (SeparationQuotient R)

Equations

• SeparationQuotient.instNonAssocRing = Function.Surjective.nonAssocRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instSemiring {R : Type u_1} [TopologicalSpace R] [Semiring R] [TopologicalSemiring R] : Semiring (SeparationQuotient R)

Equations

• SeparationQuotient.instSemiring = Function.Surjective.semiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instRing {R : Type u_1} [TopologicalSpace R] [Ring R] [TopologicalRing R] : Ring (SeparationQuotient R)

Equations

• SeparationQuotient.instRing = Function.Surjective.ring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalNonAssocCommSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocCommSemiring R] [TopologicalSemiring R] : NonUnitalNonAssocCommSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalNonAssocCommSemiring = Function.Surjective.nonUnitalNonAssocCommSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalCommSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalCommSemiring R] [TopologicalSemiring R] : NonUnitalCommSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalCommSemiring = Function.Surjective.nonUnitalCommSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instCommSemiring {R : Type u_1} [TopologicalSpace R] [CommSemiring R] [TopologicalSemiring R] : CommSemiring (SeparationQuotient R)

Equations

• SeparationQuotient.instCommSemiring = Function.Surjective.commSemiring SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• SeparationQuotient.instHasDistribNeg = Function.Surjective.hasDistribNeg SeparationQuotient.mk ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalNonAssocCommRing {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocCommRing R] [TopologicalRing R] : NonUnitalNonAssocCommRing (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalNonAssocCommRing = Function.Surjective.nonUnitalNonAssocCommRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instNonUnitalCommRing {R : Type u_1} [TopologicalSpace R] [NonUnitalCommRing R] [TopologicalRing R] : NonUnitalCommRing (SeparationQuotient R)

Equations

• SeparationQuotient.instNonUnitalCommRing = Function.Surjective.nonUnitalCommRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance SeparationQuotient.instCommRing {R : Type u_1} [TopologicalSpace R] [CommRing R] [TopologicalRing R] : CommRing (SeparationQuotient R)

Equations

• SeparationQuotient.instCommRing = Function.Surjective.commRing SeparationQuotient.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

• SeparationQuotient.instDistribSMul = Function.Surjective.distribSMul SeparationQuotient.mkAddMonoidHom ⋯ ⋯

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

• SeparationQuotient.instDistribMulAction = Function.Surjective.distribMulAction SeparationQuotient.mkAddMonoidHom ⋯ ⋯

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

• SeparationQuotient.instMulDistribMulAction = Function.Surjective.mulDistribMulAction SeparationQuotient.mkMonoidHom ⋯ ⋯

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

Equations

• SeparationQuotient.instModule = Function.Surjective.module R SeparationQuotient.mkAddMonoidHom ⋯ ⋯

@[simp]

theorem SeparationQuotient.mkCLM_apply (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] : ∀ (a : M), (SeparationQuotient.mkCLM R M) a = SeparationQuotient.mk a

@[simp]

theorem SeparationQuotient.mkCLM_toFun (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] : ∀ (a : M), (SeparationQuotient.mkCLM R M) a = SeparationQuotient.mk a

def SeparationQuotient.mkCLM (R : Type u_1) (M : Type u_2) [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

• SeparationQuotient.mkCLM R M = { toFun := SeparationQuotient.mk, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem SeparationQuotient.exists_out_continuousLinearMap (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : ∃ (f : SeparationQuotient E →L[K] E), (SeparationQuotient.mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

There exists a continuous K-linear map from SeparationQuotient E to E such that mk (outCLM x) = x for all x.

Note that continuity of this map comes for free, because mk is a topology inducing map.

noncomputable def SeparationQuotient.outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : SeparationQuotient E →L[K] E

A continuous K-linear map from SeparationQuotient E to E such that mk (outCLM x) = x for all x.

Equations

• SeparationQuotient.outCLM K E = ⋯.choose

@[simp]

theorem SeparationQuotient.mkCLM_comp_outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : (SeparationQuotient.mkCLM K E).comp (SeparationQuotient.outCLM K E) = ContinuousLinearMap.id K (SeparationQuotient E)

@[simp]

theorem SeparationQuotient.mk_outCLM (K : Type u_1) {E : Type u_2} [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] (x : SeparationQuotient E) : SeparationQuotient.mk ((SeparationQuotient.outCLM K E) x) = x

@[simp]

theorem SeparationQuotient.mk_comp_outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : SeparationQuotient.mk ∘ ⇑(SeparationQuotient.outCLM K E) = id

theorem SeparationQuotient.outCLM_embedding (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : Embedding ⇑(SeparationQuotient.outCLM K E)

The SeparationQuotient.outCLM K E map is a topological embedding.

theorem SeparationQuotient.outCLM_injective (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul K E] : Function.Injective ⇑(SeparationQuotient.outCLM K E)

theorem SeparationQuotient.outCLM_uniformInducing (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul K E] : UniformInducing ⇑(SeparationQuotient.outCLM K E)

theorem SeparationQuotient.outCLM_uniformEmbedding (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul K E] : UniformEmbedding ⇑(SeparationQuotient.outCLM K E)

theorem SeparationQuotient.outCLM_uniformContinuous (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul K E] : UniformContinuous ⇑(SeparationQuotient.outCLM K E)