Documentation

Mathlib.Logic.Function.Conjugate

Semiconjugate and commuting maps #

We define the following predicates:

def Function.Semiconj {α : Type u_1} {β : Type u_2} (f : αβ) (ga : αα) (gb : ββ) :

We say that f : α → β semiconjugates ga : α → α to gb : β → β if f ∘ ga = gb ∘ f. We use ∀ x, f (ga x) = gb (f x) as the definition, so given h : Function.Semiconj f ga gb and a : α, we have h a : f (ga a) = gb (f a) and h.comp_eq : f ∘ ga = gb ∘ f.

Equations
Instances For
    theorem Function.semiconj_iff_comp_eq {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} :
    Function.Semiconj f ga gb f ga = gb f

    Definition of Function.Semiconj in terms of functional equality.

    theorem Function.Semiconj.comp_eq {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} :
    Function.Semiconj f ga gbf ga = gb f

    Alias of the forward direction of Function.semiconj_iff_comp_eq.


    Definition of Function.Semiconj in terms of functional equality.

    theorem Function.Semiconj.eq {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) (x : α) :
    f (ga x) = gb (f x)
    theorem Function.Semiconj.comp_right {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {ga' : αα} {gb : ββ} {gb' : ββ} (h : Function.Semiconj f ga gb) (h' : Function.Semiconj f ga' gb') :
    Function.Semiconj f (ga ga') (gb gb')

    If f semiconjugates ga to gb and ga' to gb', then it semiconjugates ga ∘ ga' to gb ∘ gb'.

    theorem Function.Semiconj.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : αβ} {fbc : βγ} {ga : αα} {gb : ββ} {gc : γγ} (hab : Function.Semiconj fab ga gb) (hbc : Function.Semiconj fbc gb gc) :
    Function.Semiconj (fbc fab) ga gc

    If fab : α → β semiconjugates ga to gb and fbc : β → γ semiconjugates gb to gc, then fbc ∘ fab semiconjugates ga to gc.

    See also Function.Semiconj.comp_left for a version with reversed arguments.

    theorem Function.Semiconj.comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : αβ} {fbc : βγ} {ga : αα} {gb : ββ} {gc : γγ} (hbc : Function.Semiconj fbc gb gc) (hab : Function.Semiconj fab ga gb) :
    Function.Semiconj (fbc fab) ga gc

    If fbc : β → γ semiconjugates gb to gc and fab : α → β semiconjugates ga to gb, then fbc ∘ fab semiconjugates ga to gc.

    See also Function.Semiconj.trans for a version with reversed arguments.

    Backward compatibility note: before 2024/01/13, this lemma used to have the same order of arguments that Function.Semiconj.trans has now.

    theorem Function.Semiconj.id_right {α : Type u_1} {β : Type u_2} {f : αβ} :

    Any function semiconjugates the identity function to the identity function.

    theorem Function.Semiconj.id_left {α : Type u_1} {ga : αα} :

    The identity function semiconjugates any function to itself.

    theorem Function.Semiconj.inverses_right {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {ga' : αα} {gb : ββ} {gb' : ββ} (h : Function.Semiconj f ga gb) (ha : Function.RightInverse ga' ga) (hb : Function.LeftInverse gb' gb) :

    If f : α → β semiconjugates ga : α → α to gb : β → β, ga' is a right inverse of ga, and gb' is a left inverse of gb, then f semiconjugates ga' to gb' as well.

    theorem Function.Semiconj.inverse_left {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} {f' : βα} (h : Function.Semiconj f ga gb) (hf₁ : Function.LeftInverse f' f) (hf₂ : Function.RightInverse f' f) :

    If f semiconjugates ga to gb and f' is both a left and a right inverse of f, then f' semiconjugates gb to ga.

    theorem Function.Semiconj.option_map {α : Type u_1} {β : Type u_2} {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) :

    If f : α → β semiconjugates ga : α → α to gb : β → β, then Option.map f semiconjugates Option.map ga to Option.map gb.

    def Function.Commute {α : Type u_1} (f : αα) (g : αα) :

    Two maps f g : α → α commute if f (g x) = g (f x) for all x : α. Given h : Function.commute f g and a : α, we have h a : f (g a) = g (f a) and h.comp_eq : f ∘ g = g ∘ f.

    Equations
    Instances For
      theorem Function.Semiconj.commute {α : Type u_1} {f : αα} {g : αα} (h : Function.Semiconj f g g) :

      Reinterpret Function.Semiconj f g g as Function.Commute f g. These two predicates are definitionally equal but have different dot-notation lemmas.

      theorem Function.Commute.semiconj {α : Type u_1} {f : αα} {g : αα} (h : Function.Commute f g) :

      Reinterpret Function.Commute f g as Function.Semiconj f g g. These two predicates are definitionally equal but have different dot-notation lemmas.

      theorem Function.Commute.refl {α : Type u_1} (f : αα) :
      theorem Function.Commute.symm {α : Type u_1} {f : αα} {g : αα} (h : Function.Commute f g) :
      theorem Function.Commute.comp_right {α : Type u_1} {f : αα} {g : αα} {g' : αα} (h : Function.Commute f g) (h' : Function.Commute f g') :

      If f commutes with g and g', then it commutes with g ∘ g'.

      theorem Function.Commute.comp_left {α : Type u_1} {f : αα} {f' : αα} {g : αα} (h : Function.Commute f g) (h' : Function.Commute f' g) :

      If f and f' commute with g, then f ∘ f' commutes with g as well.

      theorem Function.Commute.id_right {α : Type u_1} {f : αα} :

      Any self-map commutes with the identity map.

      theorem Function.Commute.id_left {α : Type u_1} {f : αα} :

      The identity map commutes with any self-map.

      theorem Function.Commute.option_map {α : Type u_1} {f : αα} {g : αα} (h : Function.Commute f g) :

      If f commutes with g, then Option.map f commutes with Option.map g.

      def Function.Semiconj₂ {α : Type u_1} {β : Type u_2} (f : αβ) (ga : ααα) (gb : βββ) :

      A map f semiconjugates a binary operation ga to a binary operation gb if for all x, y we have f (ga x y) = gb (f x) (f y). E.g., a MonoidHom semiconjugates (*) to (*).

      Equations
      Instances For
        theorem Function.Semiconj₂.eq {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} (h : Function.Semiconj₂ f ga gb) (x : α) (y : α) :
        f (ga x y) = gb (f x) (f y)
        theorem Function.Semiconj₂.comp_eq {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} (h : Function.Semiconj₂ f ga gb) :
        theorem Function.Semiconj₂.id_left {α : Type u_1} (op : ααα) :
        theorem Function.Semiconj₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {ga : ααα} {gb : βββ} {f' : βγ} {gc : γγγ} (hf' : Function.Semiconj₂ f' gb gc) (hf : Function.Semiconj₂ f ga gb) :
        theorem Function.Semiconj₂.isAssociative_right {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} [Std.Associative ga] (h : Function.Semiconj₂ f ga gb) (h_surj : Function.Surjective f) :
        theorem Function.Semiconj₂.isAssociative_left {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} [Std.Associative gb] (h : Function.Semiconj₂ f ga gb) (h_inj : Function.Injective f) :
        theorem Function.Semiconj₂.isIdempotent_right {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} [Std.IdempotentOp ga] (h : Function.Semiconj₂ f ga gb) (h_surj : Function.Surjective f) :
        theorem Function.Semiconj₂.isIdempotent_left {α : Type u_1} {β : Type u_2} {f : αβ} {ga : ααα} {gb : βββ} [Std.IdempotentOp gb] (h : Function.Semiconj₂ f ga gb) (h_inj : Function.Injective f) :