Documentation

Mathlib.Logic.Embedding.Basic

Injective functions #

structure Function.Embedding (α : Sort u_1) (β : Sort u_2) :
Sort (max(max1u_1)u_2)

α ↪ β is a bundled injective function.

Instances For

    An embedding, a.k.a. a bundled injective function.

    Equations
    instance Function.instEmbeddingLikeEmbedding {α : Sort u} {β : Sort v} :
    EmbeddingLike (α β) α β
    Equations
    def Equiv.toEmbedding {α : Sort u} {β : Sort v} (f : α β) :
    α β

    Convert an α ≃ β to α ↪ β.

    This is also available as a coercion Equiv.coeEmbedding. The explicit Equiv.toEmbedding version is preferred though, since the coercion can have issues inferring the type of the resulting embedding. For example:

    -- Works:
    example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f.toEmbedding = s.map f := by simp
    -- Error, `f` has type `Fin 3 ≃ Fin 3` but is expected to have type `Fin 3 ↪ ?m_1 : Type ?`
    example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f = s.map f.toEmbedding := by simp
    
    Equations
    @[simp]
    theorem Equiv.coe_toEmbedding {α : Sort u} {β : Sort v} (f : α β) :
    ↑(Equiv.toEmbedding f) = f
    theorem Equiv.toEmbedding_apply {α : Sort u} {β : Sort v} (f : α β) (a : α) :
    ↑(Equiv.toEmbedding f) a = f a
    instance Equiv.coeEmbedding {α : Sort u} {β : Sort v} :
    Coe (α β) (α β)
    Equations
    • Equiv.coeEmbedding = { coe := Equiv.toEmbedding }
    instance Equiv.Perm.coeEmbedding {α : Sort u} :
    Coe (Equiv.Perm α) (α α)
    Equations
    • Equiv.Perm.coeEmbedding = Equiv.coeEmbedding
    theorem Function.Embedding.coe_injective {α : Sort u_1} {β : Sort u_2} :
    Function.Injective fun f => f
    theorem Function.Embedding.ext {α : Sort u_1} {β : Sort u_2} {f : α β} {g : α β} (h : ∀ (x : α), f x = g x) :
    f = g
    theorem Function.Embedding.ext_iff {α : Sort u_1} {β : Sort u_2} {f : α β} {g : α β} :
    (∀ (x : α), f x = g x) f = g
    @[simp]
    theorem Function.Embedding.toFun_eq_coe {α : Sort u_1} {β : Sort u_2} (f : α β) :
    f.toFun = f
    @[simp]
    theorem Function.Embedding.coeFn_mk {α : Sort u_1} {β : Sort u_2} (f : αβ) (i : Function.Injective f) :
    { toFun := f, inj' := i } = f
    @[simp]
    theorem Function.Embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α β) (inj : Function.Injective f) :
    { toFun := f, inj' := inj } = f
    theorem Function.Embedding.injective {α : Sort u_1} {β : Sort u_2} (f : α β) :
    theorem Function.Embedding.apply_eq_iff_eq {α : Sort u_1} {β : Sort u_2} (f : α β) (x : α) (y : α) :
    f x = f y x = y
    @[simp]
    theorem Function.Embedding.refl_apply (α : Sort u_1) (a : α) :
    def Function.Embedding.refl (α : Sort u_1) :
    α α

    The identity map as a Function.Embedding.

    Equations
    @[simp]
    theorem Function.Embedding.trans_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) :
    ∀ (a : α), ↑(Function.Embedding.trans f g) a = g (f a)
    def Function.Embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) :
    α γ

    Composition of f : α ↪ β and g : β ↪ γ.

    Equations
    @[simp]
    theorem Function.Embedding.congr_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
    def Function.Embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
    β δ

    Transfer an embedding along a pair of equivalences.

    Equations
    noncomputable def Function.Embedding.ofSurjective {α : Sort u_1} {β : Sort u_2} (f : βα) (hf : Function.Surjective f) :
    α β

    A right inverse surjInv of a surjective function as an Embedding.

    Equations
    noncomputable def Function.Embedding.equivOfSurjective {α : Sort u_1} {β : Sort u_2} (f : α β) (hf : Function.Surjective f) :
    α β

    Convert a surjective Embedding to an Equiv

    Equations
    def Function.Embedding.ofIsEmpty {α : Sort u_1} {β : Sort u_2} [inst : IsEmpty α] :
    α β

    There is always an embedding from an empty type.

    Equations
    • Function.Embedding.ofIsEmpty = { toFun := fun a => isEmptyElim a, inj' := (_ : ∀ (a : α) ⦃a₂ : α⦄, (fun a => isEmptyElim a) a = (fun a => isEmptyElim a) a₂a = a₂) }
    def Function.Embedding.setValue {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)] [inst : (a' : α) → Decidable (f a' = b)] :
    α β

    Change the value of an embedding f at one point. If the prescribed image is already occupied by some f a', then swap the values at these two points.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Function.Embedding.setValue_eq {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)] [inst : (a' : α) → Decidable (f a' = b)] :
    @[simp]
    theorem Function.Embedding.some_apply {α : Type u_1} :
    Function.Embedding.some = some
    def Function.Embedding.some {α : Type u_1} :
    α Option α

    Embedding into Option α using some.

    Equations
    @[simp]
    theorem Function.Embedding.optionMap_apply {α : Type u_1} {β : Type u_2} (f : α β) :
    def Function.Embedding.optionMap {α : Type u_1} {β : Type u_2} (f : α β) :

    A version of Option.map for Function.Embeddings.

    Equations
    def Function.Embedding.subtype {α : Sort u_1} (p : αProp) :

    Embedding of a Subtype.

    Equations
    @[simp]
    theorem Function.Embedding.coe_subtype {α : Sort u_1} (p : αProp) :
    ↑(Function.Embedding.subtype p) = Subtype.val
    noncomputable def Function.Embedding.quotientOut (α : Sort u_1) [s : Setoid α] :

    Quotient.out as an embedding.

    Equations
    @[simp]
    theorem Function.Embedding.coe_quotientOut (α : Sort u_1) [inst : Setoid α] :
    ↑(Function.Embedding.quotientOut α) = Quotient.out
    def Function.Embedding.punit {β : Sort u_1} (b : β) :

    Choosing an element b : β gives an embedding of punit into β.

    Equations
    @[simp]
    theorem Function.Embedding.sectl_apply (α : Type u_1) {β : Type u_2} (b : β) (a : α) :
    ↑(Function.Embedding.sectl α b) a = (a, b)
    def Function.Embedding.sectl (α : Type u_1) {β : Type u_2} (b : β) :
    α α × β

    Fixing an element b : β gives an embedding α ↪ α × β.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Function.Embedding.sectr_apply {α : Type u_1} (a : α) (β : Type u_2) (b : β) :
    ↑(Function.Embedding.sectr a β) b = (a, b)
    def Function.Embedding.sectr {α : Type u_1} (a : α) (β : Type u_2) :
    β α × β

    Fixing an element a : α gives an embedding β ↪ α × β.

    Equations
    • One or more equations did not get rendered due to their size.
    def Function.Embedding.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
    α × γ β × δ

    If e₁ and e₂ are embeddings, then so is prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b).

    Equations
    @[simp]
    theorem Function.Embedding.coe_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
    ↑(Function.Embedding.prodMap e₁ e₂) = Prod.map e₁ e₂
    def Function.Embedding.pprodMap {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) :
    PProd α γ PProd β δ

    If e₁ and e₂ are embeddings, then so is λ ⟨a, b⟩, ⟨e₁ a, e₂ b⟩ : pprod α γ → pprod β δ.

    Equations
    def Function.Embedding.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
    α γ β δ

    If e₁ and e₂ are embeddings, then so is sum.map e₁ e₂.

    Equations
    @[simp]
    theorem Function.Embedding.coe_sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
    ↑(Function.Embedding.sumMap e₁ e₂) = Sum.map e₁ e₂
    @[simp]
    theorem Function.Embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) :
    Function.Embedding.inl val = Sum.inl val
    def Function.Embedding.inl {α : Type u_1} {β : Type u_2} :
    α α β

    The embedding of α into the sum α ⊕ β.

    Equations
    • Function.Embedding.inl = { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1x = x_1) }
    @[simp]
    theorem Function.Embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) :
    Function.Embedding.inr val = Sum.inr val
    def Function.Embedding.inr {α : Type u_1} {β : Type u_2} :
    β α β

    The embedding of β into the sum α ⊕ β.

    Equations
    • Function.Embedding.inr = { toFun := Sum.inr, inj' := (_ : ∀ (x x_1 : β), Sum.inr x = Sum.inr x_1x = x_1) }
    @[simp]
    theorem Function.Embedding.sigmaMk_apply {α : Type u_1} {β : αType u_2} (a : α) (snd : β a) :
    ↑(Function.Embedding.sigmaMk a) snd = { fst := a, snd := snd }
    def Function.Embedding.sigmaMk {α : Type u_1} {β : αType u_2} (a : α) :
    β a (x : α) × β x

    Sigma.mk as an Function.Embedding.

    Equations
    @[simp]
    theorem Function.Embedding.sigmaMap_apply {α : Type u_1} {α' : Type u_2} {β : αType u_3} {β' : α'Type u_4} (f : α α') (g : (a : α) → β a β' (f a)) (x : (a : α) × β a) :
    ↑(Function.Embedding.sigmaMap f g) x = Sigma.map (f) (fun a => ↑(g a)) x
    def Function.Embedding.sigmaMap {α : Type u_1} {α' : Type u_2} {β : αType u_3} {β' : α'Type u_4} (f : α α') (g : (a : α) → β a β' (f a)) :
    (a : α) × β a (a' : α') × β' a'

    If f : α ↪ α' is an embedding and g : Π a, β α ↪ β' (f α) is a family of embeddings, then Sigma.map f g is an embedding.

    Equations
    @[simp]
    theorem Function.Embedding.piCongrRight_apply {α : Sort u_1} {β : αSort u_2} {γ : αSort u_3} (e : (a : α) → β a γ a) (f : (a : α) → β a) (a : α) :
    ↑(Function.Embedding.piCongrRight e) f a = ↑(e a) (f a)
    def Function.Embedding.piCongrRight {α : Sort u_1} {β : αSort u_2} {γ : αSort u_3} (e : (a : α) → β a γ a) :
    ((a : α) → β a) (a : α) → γ a

    Define an embedding (Π a : α, β a) ↪ (Π a : α, γ a) from a family of embeddings e : Π a, (β a ↪ γ a). This embedding sends f to λ a, e a (f a).

    Equations
    • Function.Embedding.piCongrRight e = { toFun := fun f a => ↑(e a) (f a), inj' := (_ : ∀ (x x_1 : (a : α) → β a), (fun f a => ↑(e a) (f a)) x = (fun f a => ↑(e a) (f a)) x_1x = x_1) }
    def Function.Embedding.arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) :
    (γα) γβ

    An embedding e : α ↪ β defines an embedding (γ → α) ↪ (γ → β) that sends each f to e ∘ f.

    Equations
    @[simp]
    theorem Function.Embedding.arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : γ α) :
    noncomputable def Function.Embedding.arrowCongrLeft {α : Sort u} {β : Sort v} {γ : Sort w} [inst : Inhabited γ] (e : α β) :
    (αγ) βγ

    An embedding e : α ↪ β defines an embedding (α → γ) ↪ (β → γ) for any inhabited type γ. This embedding sends each f : α → γ to a function g : β → γ such that g ∘ e = f and g y = default whenever y ∉ range e.

    Equations
    • One or more equations did not get rendered due to their size.
    def Function.Embedding.subtypeMap {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (f : α β) (h : x : α⦄ → p xq (f x)) :
    { x // p x } { y // q y }

    Restrict both domain and codomain of an embedding.

    Equations
    theorem Function.Embedding.swap_apply {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : α β) (x : α) (y : α) (z : α) :
    ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
    theorem Function.Embedding.swap_comp {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : α β) (x : α) (y : α) :
    ↑(Equiv.swap (f x) (f y)) f = f ↑(Equiv.swap x y)
    @[simp]
    theorem Equiv.asEmbedding_apply {β : Sort u_1} {α : Sort u_2} {p : βProp} (e : α Subtype p) :
    ∀ (a : α), ↑(Equiv.asEmbedding e) a = ↑(e a)
    def Equiv.asEmbedding {β : Sort u_1} {α : Sort u_2} {p : βProp} (e : α Subtype p) :
    α β

    Given an equivalence to a subtype, produce an embedding to the elements of the corresponding set.

    Equations
    def Equiv.subtypeInjectiveEquivEmbedding (α : Sort u_1) (β : Sort u_2) :
    { f // Function.Injective f } (α β)

    The type of embeddings α ↪ β is equivalent to the subtype of all injective functions α → β.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.embeddingCongr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α β) (h' : γ δ) (f : α γ) :
    def Equiv.embeddingCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α β) (h' : γ δ) :
    (α γ) (β δ)

    If α₁ ≃ α₂ and β₁ ≃ β₂, then the type of embeddings α₁ ↪ β₁ is equivalent to the type of embeddings α₂ ↪ β₂.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    @[simp]
    theorem Equiv.embeddingCongr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
    @[simp]
    theorem Equiv.embeddingCongr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
    theorem Equiv.embeddingCongr_apply_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁ β₁) (g : β₁ γ₁) :
    @[simp]
    theorem Equiv.trans_toEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
    def subtypeOrLeftEmbedding {α : Type u_1} (p : αProp) (q : αProp) [inst : DecidablePred p] :
    { x // p x q x } { x // p x } { x // q x }

    A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop can be injectively split into a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem subtypeOrLeftEmbedding_apply_left {α : Type u_1} {p : αProp} {q : αProp} [inst : DecidablePred p] (x : { x // p x q x }) (hx : p x) :
    ↑(subtypeOrLeftEmbedding p q) x = Sum.inl { val := x, property := hx }
    theorem subtypeOrLeftEmbedding_apply_right {α : Type u_1} {p : αProp} {q : αProp} [inst : DecidablePred p] (x : { x // p x q x }) (hx : ¬p x) :
    ↑(subtypeOrLeftEmbedding p q) x = Sum.inr { val := x, property := Or.resolve_left (_ : p x q x) hx }
    @[simp]
    theorem Subtype.impEmbedding_apply_coe {α : Type u_1} (p : αProp) (q : αProp) (h : (x : α) → p xq x) (x : { x // p x }) :
    ↑(↑(Subtype.impEmbedding p q h) x) = x
    def Subtype.impEmbedding {α : Type u_1} (p : αProp) (q : αProp) (h : (x : α) → p xq x) :
    { x // p x } { x // q x }

    A subtype {x // p x} can be injectively sent to into a subtype {x // q x}, if p x → q x for all x : α.

    Equations
    • One or more equations did not get rendered due to their size.