Groebner.MulEquiv

source

theorem MulEquiv.range_subtype {M : Type u_1} [MulOneClass M] (s : Submonoid M) :

Set.range ⇑s.subtype = ↑s

source

theorem AddEquiv.range_subtype {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) :

Set.range ⇑s.subtype = ↑s

source

theorem MulEquiv.range_subtype' {M : Type u_1} [MulOneClass M] (s : Submonoid M) :

↑(Set.range ⇑s.subtype) = ↥s

source

theorem AddEquiv.range_subtype' {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) :

↑(Set.range ⇑s.subtype) = ↥s

source

theorem MonoidHom.mrangeRestrict_eq_rangeFactorization {M : Type u_1} [MulOneClass M] {N : Type u_4} [MulOneClass N] (f : M →* N) :

⇑f.mrangeRestrict = Set.rangeFactorization ⇑f

source

theorem AddMonoidHom.mrangeRestrict_eq_rangeFactorization {M : Type u_1} [AddZeroClass M] {N : Type u_4} [AddZeroClass N] (f : M →+ N) :

⇑f.mrangeRestrict = Set.rangeFactorization ⇑f

source

def MulEquiv.ofLeftInverse'' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : ↥(MonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) :

M ≃* ↥(MonoidHom.mrange f)

A monoid homomorphism f : M →* N with a left-inverse g : N → M defines a multiplicative equivalence between M and f.mrange. This is a bidirectional version of MonoidHom.mrange_restrict.

Equations

MulEquiv.ofLeftInverse'' f g h = { toFun := ⇑f.mrangeRestrict, invFun := g, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.ofLeftInverse'' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : ↥(AddMonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) :

M ≃+ ↥(AddMonoidHom.mrange f)

An additive monoid homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.mrange. This is a bidirectional version of AddMonoidHom.mrange_restrict.

Equations

AddEquiv.ofLeftInverse'' f g h = { toFun := ⇑f.mrangeRestrict, invFun := g, left_inv := h, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.ofLeftInverse''_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : ↥(AddMonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) (a : M) :

(ofLeftInverse'' f g h) a = f.mrangeRestrict a

source

@[simp]

theorem MulEquiv.ofLeftInverse''_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : ↥(MonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) (a✝ : ↥(MonoidHom.mrange f)) :

(ofLeftInverse'' f g h).symm a✝ = g a✝

source

@[simp]

theorem AddEquiv.ofLeftInverse''_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : ↥(AddMonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) (a✝ : ↥(AddMonoidHom.mrange f)) :

(ofLeftInverse'' f g h).symm a✝ = g a✝

source

@[simp]

theorem MulEquiv.ofLeftInverse''_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : ↥(MonoidHom.mrange f) → M) (h : Function.LeftInverse g ⇑f.mrangeRestrict) (a : M) :

(ofLeftInverse'' f g h) a = f.mrangeRestrict a

source

@[simp]

theorem Function.LeftInverse.of_subsingleton {α : Sort u_4} {β : Sort u_5} [Subsingleton β] (g : α → β) (f : β → α) :

LeftInverse g f

source

@[simp]

theorem Function.RightInverse.of_subsingleton {α : Sort u_4} [Subsingleton α] {β : Sort u_5} (g : α → β) (f : β → α) :

RightInverse g f

source

@[simp]

theorem Function.LeftInverse.of_empty {α : Sort u_4} [IsEmpty α] {β : Sort u_5} (g : α → β) (f : β → α) :

LeftInverse g f

source

@[simp]

theorem Function.RightInverse.of_empty {α : Sort u_4} {β : Sort u_5} [IsEmpty β] (g : α → β) (f : β → α) :

RightInverse g f

source

theorem Set.leftInverse_rangeFactorization {α : Type u_1} {β : Type u_2} (f : α → β) :

Function.LeftInverse (rangeSplitting f) (rangeFactorization f) ↔ Function.Injective f