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.

@[implicit_reducible]

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

@[implicit_reducible]

instance SeparationQuotient.instVAdd {M : Type u_1} {X : Type u_2} [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] : VAdd M (SeparationQuotient 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) : mk (c • x) = c • mk 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) : mk (c +ᵥ x) = c +ᵥ mk x

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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

@[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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

SeparationQuotient.mk as a MonoidHom.

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

SeparationQuotient.mk as an AddMonoidHom.

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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

@[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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

SeparationQuotient.mk as a RingHom.

@[simp]

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

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

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.

@[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✝

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.

@[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✝

@[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

@[implicit_reducible]

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)

@[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