Documentation

Mathlib.Order.Hom.CompleteLattice

Complete lattice homomorphisms #

This file defines frame homomorphisms and complete lattice homomorphisms.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

Typeclasses #

Concrete homs #

TODO #

Frame homs are Heyting homs.

structure sSupHom (α : Type u_8) (β : Type u_9) [SupSet α] [SupSet β] :
Type (max u_8 u_9)

The type of -preserving functions from α to β.

  • toFun : αβ

    The underlying function of a sSupHom.

  • map_sSup' : ∀ (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)

    The proposition that a sSupHom commutes with arbitrary suprema/joins.

Instances For
    theorem sSupHom.map_sSup' {α : Type u_8} {β : Type u_9} [SupSet α] [SupSet β] (self : sSupHom α β) (s : Set α) :
    self.toFun (sSup s) = sSup (self.toFun '' s)

    The proposition that a sSupHom commutes with arbitrary suprema/joins.

    structure sInfHom (α : Type u_8) (β : Type u_9) [InfSet α] [InfSet β] :
    Type (max u_8 u_9)

    The type of -preserving functions from α to β.

    • toFun : αβ

      The underlying function of an sInfHom.

    • map_sInf' : ∀ (s : Set α), self.toFun (sInf s) = sInf (self.toFun '' s)

      The proposition that a sInfHom commutes with arbitrary infima/meets

    Instances For
      theorem sInfHom.map_sInf' {α : Type u_8} {β : Type u_9} [InfSet α] [InfSet β] (self : sInfHom α β) (s : Set α) :
      self.toFun (sInf s) = sInf (self.toFun '' s)

      The proposition that a sInfHom commutes with arbitrary infima/meets

      structure FrameHom (α : Type u_8) (β : Type u_9) [CompleteLattice α] [CompleteLattice β] extends InfTopHom :
      Type (max u_8 u_9)

      The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.

      • toFun : αβ
      • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
      • map_top' : self.toFun =
      • map_sSup' : ∀ (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)

        The proposition that frame homomorphisms commute with arbitrary suprema/joins.

      Instances For
        theorem FrameHom.map_sSup' {α : Type u_8} {β : Type u_9} [CompleteLattice α] [CompleteLattice β] (self : FrameHom α β) (s : Set α) :
        self.toFun (sSup s) = sSup (self.toFun '' s)

        The proposition that frame homomorphisms commute with arbitrary suprema/joins.

        structure CompleteLatticeHom (α : Type u_8) (β : Type u_9) [CompleteLattice α] [CompleteLattice β] extends sInfHom :
        Type (max u_8 u_9)

        The type of complete lattice homomorphisms from α to β.

        • toFun : αβ
        • map_sInf' : ∀ (s : Set α), self.toFun (sInf s) = sInf (self.toFun '' s)
        • map_sSup' : ∀ (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)

          The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.

        Instances For
          theorem CompleteLatticeHom.map_sSup' {α : Type u_8} {β : Type u_9} [CompleteLattice α] [CompleteLattice β] (self : CompleteLatticeHom α β) (s : Set α) :
          self.toFun (sSup s) = sSup (self.toFun '' s)

          The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.

          class sSupHomClass (F : Type u_8) (α : Type u_9) (β : Type u_10) [SupSet α] [SupSet β] [FunLike F α β] :

          sSupHomClass F α β states that F is a type of -preserving morphisms.

          You should extend this class when you extend sSupHom.

          • map_sSup : ∀ (f : F) (s : Set α), f (sSup s) = sSup (f '' s)

            The proposition that members of sSupHomClasss commute with arbitrary suprema/joins.

          Instances
            @[simp]
            theorem sSupHomClass.map_sSup {F : Type u_8} {α : Type u_9} {β : Type u_10} [SupSet α] [SupSet β] [FunLike F α β] [self : sSupHomClass F α β] (f : F) (s : Set α) :
            f (sSup s) = sSup (f '' s)

            The proposition that members of sSupHomClasss commute with arbitrary suprema/joins.

            class sInfHomClass (F : Type u_8) (α : Type u_9) (β : Type u_10) [InfSet α] [InfSet β] [FunLike F α β] :

            sInfHomClass F α β states that F is a type of -preserving morphisms.

            You should extend this class when you extend sInfHom.

            • map_sInf : ∀ (f : F) (s : Set α), f (sInf s) = sInf (f '' s)

              The proposition that members of sInfHomClasss commute with arbitrary infima/meets.

            Instances
              @[simp]
              theorem sInfHomClass.map_sInf {F : Type u_8} {α : Type u_9} {β : Type u_10} [InfSet α] [InfSet β] [FunLike F α β] [self : sInfHomClass F α β] (f : F) (s : Set α) :
              f (sInf s) = sInf (f '' s)

              The proposition that members of sInfHomClasss commute with arbitrary infima/meets.

              class FrameHomClass (F : Type u_8) (α : Type u_9) (β : Type u_10) [CompleteLattice α] [CompleteLattice β] [FunLike F α β] extends InfTopHomClass :

              FrameHomClass F α β states that F is a type of frame morphisms. They preserve and .

              You should extend this class when you extend FrameHom.

              • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
              • map_top : ∀ (f : F), f =
              • map_sSup : ∀ (f : F) (s : Set α), f (sSup s) = sSup (f '' s)

                The proposition that members of FrameHomClass commute with arbitrary suprema/joins.

              Instances
                theorem FrameHomClass.map_sSup {F : Type u_8} {α : Type u_9} {β : Type u_10} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [self : FrameHomClass F α β] (f : F) (s : Set α) :
                f (sSup s) = sSup (f '' s)

                The proposition that members of FrameHomClass commute with arbitrary suprema/joins.

                class CompleteLatticeHomClass (F : Type u_8) (α : Type u_9) (β : Type u_10) [CompleteLattice α] [CompleteLattice β] [FunLike F α β] extends sInfHomClass :

                CompleteLatticeHomClass F α β states that F is a type of complete lattice morphisms.

                You should extend this class when you extend CompleteLatticeHom.

                Instances
                  theorem CompleteLatticeHomClass.map_sSup {F : Type u_8} {α : Type u_9} {β : Type u_10} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [self : CompleteLatticeHomClass F α β] (f : F) (s : Set α) :
                  f (sSup s) = sSup (f '' s)

                  The proposition that members of CompleteLatticeHomClass commute with arbitrary suprema/joins.

                  @[simp]
                  theorem map_iSup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [FunLike F α β] [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ια) :
                  f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
                  theorem map_iSup₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ιSort u_7} [FunLike F α β] [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : (i : ι) → κ iα) :
                  f (⨆ (i : ι), ⨆ (j : κ i), g i j) = ⨆ (i : ι), ⨆ (j : κ i), f (g i j)
                  @[simp]
                  theorem map_iInf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [FunLike F α β] [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ια) :
                  f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
                  theorem map_iInf₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ιSort u_7} [FunLike F α β] [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : (i : ι) → κ iα) :
                  f (⨅ (i : ι), ⨅ (j : κ i), g i j) = ⨅ (i : ι), ⨅ (j : κ i), f (g i j)
                  @[instance 100]
                  instance sSupHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] :
                  Equations
                  • =
                  @[instance 100]
                  instance sInfHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [sInfHomClass F α β] :
                  Equations
                  • =
                  @[instance 100]
                  instance FrameHomClass.tosSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] :
                  sSupHomClass F α β
                  Equations
                  • =
                  @[instance 100]
                  instance FrameHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] :
                  Equations
                  • =
                  @[instance 100]
                  instance CompleteLatticeHomClass.toFrameHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] :
                  Equations
                  • =
                  @[instance 100]
                  Equations
                  • =
                  @[instance 100]
                  instance OrderIsoClass.tosSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
                  sSupHomClass F α β
                  Equations
                  • =
                  @[instance 100]
                  instance OrderIsoClass.tosInfHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
                  sInfHomClass F α β
                  Equations
                  • =
                  @[instance 100]
                  instance OrderIsoClass.toCompleteLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
                  Equations
                  • =
                  @[simp]
                  theorem OrderIso.toCompleteLatticeHom_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (a : α) :
                  f.toCompleteLatticeHom.toFun a = f a
                  def OrderIso.toCompleteLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) :

                  Reinterpret an order isomorphism as a morphism of complete lattices.

                  Equations
                  • f.toCompleteLatticeHom = { toFun := f, map_sInf' := , map_sSup' := }
                  Instances For
                    instance instCoeTCSSupHomOfSSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [SupSet α] [SupSet β] [sSupHomClass F α β] :
                    CoeTC F (sSupHom α β)
                    Equations
                    • instCoeTCSSupHomOfSSupHomClass = { coe := fun (f : F) => { toFun := f, map_sSup' := } }
                    instance instCoeTCSInfHomOfSInfHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [InfSet α] [InfSet β] [sInfHomClass F α β] :
                    CoeTC F (sInfHom α β)
                    Equations
                    • instCoeTCSInfHomOfSInfHomClass = { coe := fun (f : F) => { toFun := f, map_sInf' := } }
                    instance instCoeTCFrameHomOfFrameHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] :
                    CoeTC F (FrameHom α β)
                    Equations
                    • instCoeTCFrameHomOfFrameHomClass = { coe := fun (f : F) => { toFun := f, map_inf' := , map_top' := , map_sSup' := } }
                    Equations
                    • instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass = { coe := fun (f : F) => { toFun := f, map_sInf' := , map_sSup' := } }

                    Supremum homomorphisms #

                    instance sSupHom.instFunLike {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] :
                    FunLike (sSupHom α β) α β
                    Equations
                    • sSupHom.instFunLike = { coe := sSupHom.toFun, coe_injective' := }
                    instance sSupHom.instSSupHomClass {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] :
                    sSupHomClass (sSupHom α β) α β
                    Equations
                    • =
                    @[simp]
                    theorem sSupHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) :
                    f.toFun = f
                    @[simp]
                    theorem sSupHom.coe_mk {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : αβ) (hf : ∀ (s : Set α), f (sSup s) = sSup (f '' s)) :
                    { toFun := f, map_sSup' := hf } = f
                    theorem sSupHom.ext {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] {f : sSupHom α β} {g : sSupHom α β} (h : ∀ (a : α), f a = g a) :
                    f = g
                    def sSupHom.copy {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : αβ) (h : f' = f) :
                    sSupHom α β

                    Copy of a sSupHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                    Equations
                    • f.copy f' h = { toFun := f', map_sSup' := }
                    Instances For
                      @[simp]
                      theorem sSupHom.coe_copy {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : αβ) (h : f' = f) :
                      (f.copy f' h) = f'
                      theorem sSupHom.copy_eq {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : αβ) (h : f' = f) :
                      f.copy f' h = f
                      def sSupHom.id (α : Type u_2) [SupSet α] :
                      sSupHom α α

                      id as a sSupHom.

                      Equations
                      Instances For
                        instance sSupHom.instInhabited (α : Type u_2) [SupSet α] :
                        Equations
                        @[simp]
                        theorem sSupHom.coe_id (α : Type u_2) [SupSet α] :
                        (sSupHom.id α) = id
                        @[simp]
                        theorem sSupHom.id_apply {α : Type u_2} [SupSet α] (a : α) :
                        (sSupHom.id α) a = a
                        def sSupHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (f : sSupHom β γ) (g : sSupHom α β) :
                        sSupHom α γ

                        Composition of sSupHoms as a sSupHom.

                        Equations
                        • f.comp g = { toFun := f g, map_sSup' := }
                        Instances For
                          @[simp]
                          theorem sSupHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (f : sSupHom β γ) (g : sSupHom α β) :
                          (f.comp g) = f g
                          @[simp]
                          theorem sSupHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (f : sSupHom β γ) (g : sSupHom α β) (a : α) :
                          (f.comp g) a = f (g a)
                          @[simp]
                          theorem sSupHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [SupSet α] [SupSet β] [SupSet γ] [SupSet δ] (f : sSupHom γ δ) (g : sSupHom β γ) (h : sSupHom α β) :
                          (f.comp g).comp h = f.comp (g.comp h)
                          @[simp]
                          theorem sSupHom.comp_id {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) :
                          f.comp (sSupHom.id α) = f
                          @[simp]
                          theorem sSupHom.id_comp {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) :
                          (sSupHom.id β).comp f = f
                          @[simp]
                          theorem sSupHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] {g₁ : sSupHom β γ} {g₂ : sSupHom β γ} {f : sSupHom α β} (hf : Function.Surjective f) :
                          g₁.comp f = g₂.comp f g₁ = g₂
                          @[simp]
                          theorem sSupHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] {g : sSupHom β γ} {f₁ : sSupHom α β} {f₂ : sSupHom α β} (hg : Function.Injective g) :
                          g.comp f₁ = g.comp f₂ f₁ = f₂
                          instance sSupHom.instPartialOrder {α : Type u_2} {β : Type u_3} [SupSet α] :
                          {x : CompleteLattice β} → PartialOrder (sSupHom α β)
                          Equations
                          instance sSupHom.instBot {α : Type u_2} {β : Type u_3} [SupSet α] :
                          {x : CompleteLattice β} → Bot (sSupHom α β)
                          Equations
                          • sSupHom.instBot = { bot := { toFun := fun (x_1 : α) => , map_sSup' := } }
                          instance sSupHom.instOrderBot {α : Type u_2} {β : Type u_3} [SupSet α] :
                          {x : CompleteLattice β} → OrderBot (sSupHom α β)
                          Equations
                          @[simp]
                          theorem sSupHom.coe_bot {α : Type u_2} {β : Type u_3} [SupSet α] :
                          ∀ {x : CompleteLattice β}, =
                          @[simp]
                          theorem sSupHom.bot_apply {α : Type u_2} {β : Type u_3} [SupSet α] :
                          ∀ {x : CompleteLattice β} (a : α), a =

                          Infimum homomorphisms #

                          instance sInfHom.instFunLike {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] :
                          FunLike (sInfHom α β) α β
                          Equations
                          • sInfHom.instFunLike = { coe := sInfHom.toFun, coe_injective' := }
                          instance sInfHom.instSInfHomClass {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] :
                          sInfHomClass (sInfHom α β) α β
                          Equations
                          • =
                          @[simp]
                          theorem sInfHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) :
                          f.toFun = f
                          @[simp]
                          theorem sInfHom.coe_mk {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : αβ) (hf : ∀ (s : Set α), f (sInf s) = sInf (f '' s)) :
                          { toFun := f, map_sInf' := hf } = f
                          theorem sInfHom.ext {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] {f : sInfHom α β} {g : sInfHom α β} (h : ∀ (a : α), f a = g a) :
                          f = g
                          def sInfHom.copy {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : αβ) (h : f' = f) :
                          sInfHom α β

                          Copy of a sInfHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                          Equations
                          • f.copy f' h = { toFun := f', map_sInf' := }
                          Instances For
                            @[simp]
                            theorem sInfHom.coe_copy {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : αβ) (h : f' = f) :
                            (f.copy f' h) = f'
                            theorem sInfHom.copy_eq {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : αβ) (h : f' = f) :
                            f.copy f' h = f
                            def sInfHom.id (α : Type u_2) [InfSet α] :
                            sInfHom α α

                            id as an sInfHom.

                            Equations
                            Instances For
                              instance sInfHom.instInhabited (α : Type u_2) [InfSet α] :
                              Equations
                              @[simp]
                              theorem sInfHom.coe_id (α : Type u_2) [InfSet α] :
                              (sInfHom.id α) = id
                              @[simp]
                              theorem sInfHom.id_apply {α : Type u_2} [InfSet α] (a : α) :
                              (sInfHom.id α) a = a
                              def sInfHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (f : sInfHom β γ) (g : sInfHom α β) :
                              sInfHom α γ

                              Composition of sInfHoms as a sInfHom.

                              Equations
                              • f.comp g = { toFun := f g, map_sInf' := }
                              Instances For
                                @[simp]
                                theorem sInfHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (f : sInfHom β γ) (g : sInfHom α β) :
                                (f.comp g) = f g
                                @[simp]
                                theorem sInfHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (f : sInfHom β γ) (g : sInfHom α β) (a : α) :
                                (f.comp g) a = f (g a)
                                @[simp]
                                theorem sInfHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [InfSet α] [InfSet β] [InfSet γ] [InfSet δ] (f : sInfHom γ δ) (g : sInfHom β γ) (h : sInfHom α β) :
                                (f.comp g).comp h = f.comp (g.comp h)
                                @[simp]
                                theorem sInfHom.comp_id {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) :
                                f.comp (sInfHom.id α) = f
                                @[simp]
                                theorem sInfHom.id_comp {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) :
                                (sInfHom.id β).comp f = f
                                @[simp]
                                theorem sInfHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] {g₁ : sInfHom β γ} {g₂ : sInfHom β γ} {f : sInfHom α β} (hf : Function.Surjective f) :
                                g₁.comp f = g₂.comp f g₁ = g₂
                                @[simp]
                                theorem sInfHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] {g : sInfHom β γ} {f₁ : sInfHom α β} {f₂ : sInfHom α β} (hg : Function.Injective g) :
                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                instance sInfHom.instPartialOrder {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] :
                                Equations
                                instance sInfHom.instTop {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] :
                                Top (sInfHom α β)
                                Equations
                                • sInfHom.instTop = { top := { toFun := fun (x : α) => , map_sInf' := } }
                                instance sInfHom.instOrderTop {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] :
                                Equations
                                @[simp]
                                theorem sInfHom.coe_top {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] :
                                =
                                @[simp]
                                theorem sInfHom.top_apply {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] (a : α) :

                                Frame homomorphisms #

                                instance FrameHom.instFunLike {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] :
                                FunLike (FrameHom α β) α β
                                Equations
                                • FrameHom.instFunLike = { coe := fun (f : FrameHom α β) => f.toFun, coe_injective' := }
                                instance FrameHom.instFrameHomClass {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] :
                                FrameHomClass (FrameHom α β) α β
                                Equations
                                • =
                                def FrameHom.toLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :

                                Reinterpret a FrameHom as a LatticeHom.

                                Equations
                                • f.toLatticeHom = { toFun := f, map_sup' := , map_inf' := }
                                Instances For
                                  theorem FrameHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :
                                  f.toFun = f
                                  @[simp]
                                  theorem FrameHom.coe_toInfTopHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :
                                  f.toInfTopHom = f
                                  @[simp]
                                  theorem FrameHom.coe_toLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :
                                  f.toLatticeHom = f
                                  @[simp]
                                  theorem FrameHom.coe_mk {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : InfTopHom α β) (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)) :
                                  { toInfTopHom := f, map_sSup' := hf } = f
                                  theorem FrameHom.ext {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : FrameHom α β} {g : FrameHom α β} (h : ∀ (a : α), f a = g a) :
                                  f = g
                                  def FrameHom.copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : αβ) (h : f' = f) :
                                  FrameHom α β

                                  Copy of a FrameHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                  Equations
                                  • f.copy f' h = let __src := { toFun := f, map_sSup' := }.copy f' h; { toInfTopHom := f.copy f' h, map_sSup' := }
                                  Instances For
                                    @[simp]
                                    theorem FrameHom.coe_copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : αβ) (h : f' = f) :
                                    (f.copy f' h) = f'
                                    theorem FrameHom.copy_eq {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : αβ) (h : f' = f) :
                                    f.copy f' h = f
                                    def FrameHom.id (α : Type u_2) [CompleteLattice α] :
                                    FrameHom α α

                                    id as a FrameHom.

                                    Equations
                                    Instances For
                                      Equations
                                      @[simp]
                                      theorem FrameHom.coe_id (α : Type u_2) [CompleteLattice α] :
                                      (FrameHom.id α) = id
                                      @[simp]
                                      theorem FrameHom.id_apply {α : Type u_2} [CompleteLattice α] (a : α) :
                                      (FrameHom.id α) a = a
                                      def FrameHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) :
                                      FrameHom α γ

                                      Composition of FrameHoms as a FrameHom.

                                      Equations
                                      • f.comp g = let __src := { toFun := f, map_sSup' := }.comp { toFun := g, map_sSup' := }; { toInfTopHom := f.comp g.toInfTopHom, map_sSup' := }
                                      Instances For
                                        @[simp]
                                        theorem FrameHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) :
                                        (f.comp g) = f g
                                        @[simp]
                                        theorem FrameHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) (a : α) :
                                        (f.comp g) a = f (g a)
                                        @[simp]
                                        theorem FrameHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] [CompleteLattice δ] (f : FrameHom γ δ) (g : FrameHom β γ) (h : FrameHom α β) :
                                        (f.comp g).comp h = f.comp (g.comp h)
                                        @[simp]
                                        theorem FrameHom.comp_id {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :
                                        f.comp (FrameHom.id α) = f
                                        @[simp]
                                        theorem FrameHom.id_comp {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) :
                                        (FrameHom.id β).comp f = f
                                        @[simp]
                                        theorem FrameHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {g₁ : FrameHom β γ} {g₂ : FrameHom β γ} {f : FrameHom α β} (hf : Function.Surjective f) :
                                        g₁.comp f = g₂.comp f g₁ = g₂
                                        @[simp]
                                        theorem FrameHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {g : FrameHom β γ} {f₁ : FrameHom α β} {f₂ : FrameHom α β} (hg : Function.Injective g) :
                                        g.comp f₁ = g.comp f₂ f₁ = f₂
                                        instance FrameHom.instPartialOrder {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] :
                                        Equations

                                        Complete lattice homomorphisms #

                                        instance CompleteLatticeHom.instFunLike {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] :
                                        Equations
                                        • CompleteLatticeHom.instFunLike = { coe := fun (f : CompleteLatticeHom α β) => f.toFun, coe_injective' := }
                                        def CompleteLatticeHom.tosSupHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                        sSupHom α β

                                        Reinterpret a CompleteLatticeHom as a sSupHom.

                                        Equations
                                        • f.tosSupHom = { toFun := f, map_sSup' := }
                                        Instances For

                                          Reinterpret a CompleteLatticeHom as a BoundedLatticeHom.

                                          Equations
                                          • f.toBoundedLatticeHom = let __src := { toFun := f, map_sup' := , map_inf' := }; { toFun := f, map_sup' := , map_inf' := , map_top' := , map_bot' := }
                                          Instances For
                                            theorem CompleteLatticeHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                            f.toFun = f
                                            @[simp]
                                            theorem CompleteLatticeHom.coe_tosInfHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                            f.tosInfHom = f
                                            @[simp]
                                            theorem CompleteLatticeHom.coe_tosSupHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                            f.tosSupHom = f
                                            @[simp]
                                            theorem CompleteLatticeHom.coe_toBoundedLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                            f.toBoundedLatticeHom = f
                                            @[simp]
                                            theorem CompleteLatticeHom.coe_mk {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : sInfHom α β) (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)) :
                                            { tosInfHom := f, map_sSup' := hf } = f
                                            theorem CompleteLatticeHom.ext {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : CompleteLatticeHom α β} {g : CompleteLatticeHom α β} (h : ∀ (a : α), f a = g a) :
                                            f = g
                                            def CompleteLatticeHom.copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : αβ) (h : f' = f) :

                                            Copy of a CompleteLatticeHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                            Equations
                                            • f.copy f' h = let __src := f.tosSupHom.copy f' h; { tosInfHom := f.copy f' h, map_sSup' := }
                                            Instances For
                                              @[simp]
                                              theorem CompleteLatticeHom.coe_copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : αβ) (h : f' = f) :
                                              (f.copy f' h) = f'
                                              theorem CompleteLatticeHom.copy_eq {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : αβ) (h : f' = f) :
                                              f.copy f' h = f

                                              id as a CompleteLatticeHom.

                                              Equations
                                              Instances For
                                                @[simp]
                                                @[simp]
                                                theorem CompleteLatticeHom.id_apply {α : Type u_2} [CompleteLattice α] (a : α) :
                                                def CompleteLatticeHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) :

                                                Composition of CompleteLatticeHoms as a CompleteLatticeHom.

                                                Equations
                                                • f.comp g = let __src := f.tosSupHom.comp g.tosSupHom; { tosInfHom := f.comp g.tosInfHom, map_sSup' := }
                                                Instances For
                                                  @[simp]
                                                  theorem CompleteLatticeHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) :
                                                  (f.comp g) = f g
                                                  @[simp]
                                                  theorem CompleteLatticeHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) (a : α) :
                                                  (f.comp g) a = f (g a)
                                                  @[simp]
                                                  theorem CompleteLatticeHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] [CompleteLattice δ] (f : CompleteLatticeHom γ δ) (g : CompleteLatticeHom β γ) (h : CompleteLatticeHom α β) :
                                                  (f.comp g).comp h = f.comp (g.comp h)
                                                  @[simp]
                                                  theorem CompleteLatticeHom.comp_id {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                                  f.comp (CompleteLatticeHom.id α) = f
                                                  @[simp]
                                                  theorem CompleteLatticeHom.id_comp {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                                  (CompleteLatticeHom.id β).comp f = f
                                                  @[simp]
                                                  theorem CompleteLatticeHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {g₁ : CompleteLatticeHom β γ} {g₂ : CompleteLatticeHom β γ} {f : CompleteLatticeHom α β} (hf : Function.Surjective f) :
                                                  g₁.comp f = g₂.comp f g₁ = g₂
                                                  @[simp]
                                                  theorem CompleteLatticeHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {g : CompleteLatticeHom β γ} {f₁ : CompleteLatticeHom α β} {f₂ : CompleteLatticeHom α β} (hg : Function.Injective g) :
                                                  g.comp f₁ = g.comp f₂ f₁ = f₂

                                                  Dual homs #

                                                  @[simp]
                                                  theorem sSupHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sInfHom αᵒᵈ βᵒᵈ) :
                                                  ∀ (a : α), (sSupHom.dual.symm f) a = (OrderDual.ofDual f OrderDual.toDual) a
                                                  @[simp]
                                                  theorem sSupHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) :
                                                  ∀ (a : αᵒᵈ), (sSupHom.dual f).toFun a = (OrderDual.toDual f OrderDual.ofDual) a
                                                  def sSupHom.dual {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] :

                                                  Reinterpret a -homomorphism as an -homomorphism between the dual orders.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem sSupHom.dual_id {α : Type u_2} [SupSet α] :
                                                    sSupHom.dual (sSupHom.id α) = sInfHom.id αᵒᵈ
                                                    @[simp]
                                                    theorem sSupHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (g : sSupHom β γ) (f : sSupHom α β) :
                                                    sSupHom.dual (g.comp f) = (sSupHom.dual g).comp (sSupHom.dual f)
                                                    @[simp]
                                                    theorem sSupHom.symm_dual_id {α : Type u_2} [SupSet α] :
                                                    sSupHom.dual.symm (sInfHom.id αᵒᵈ) = sSupHom.id α
                                                    @[simp]
                                                    theorem sSupHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (g : sInfHom βᵒᵈ γᵒᵈ) (f : sInfHom αᵒᵈ βᵒᵈ) :
                                                    sSupHom.dual.symm (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)
                                                    @[simp]
                                                    theorem sInfHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) :
                                                    ∀ (a : αᵒᵈ), (sInfHom.dual f) a = (OrderDual.toDual f OrderDual.ofDual) a
                                                    @[simp]
                                                    theorem sInfHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sSupHom αᵒᵈ βᵒᵈ) :
                                                    ∀ (a : α), (sInfHom.dual.symm f).toFun a = (OrderDual.ofDual f OrderDual.toDual) a
                                                    def sInfHom.dual {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] :

                                                    Reinterpret an -homomorphism as a -homomorphism between the dual orders.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem sInfHom.dual_id {α : Type u_2} [InfSet α] :
                                                      sInfHom.dual (sInfHom.id α) = sSupHom.id αᵒᵈ
                                                      @[simp]
                                                      theorem sInfHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (g : sInfHom β γ) (f : sInfHom α β) :
                                                      sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f)
                                                      @[simp]
                                                      theorem sInfHom.symm_dual_id {α : Type u_2} [InfSet α] :
                                                      sInfHom.dual.symm (sSupHom.id αᵒᵈ) = sInfHom.id α
                                                      @[simp]
                                                      theorem sInfHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (g : sSupHom βᵒᵈ γᵒᵈ) (f : sSupHom αᵒᵈ βᵒᵈ) :
                                                      sInfHom.dual.symm (g.comp f) = (sInfHom.dual.symm g).comp (sInfHom.dual.symm f)
                                                      @[simp]
                                                      theorem CompleteLatticeHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom αᵒᵈ βᵒᵈ) :
                                                      ∀ (a : αᵒᵈᵒᵈ), (CompleteLatticeHom.dual.symm f).toFun a = OrderDual.toDual (f (OrderDual.ofDual a))
                                                      @[simp]
                                                      theorem CompleteLatticeHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) :
                                                      ∀ (a : αᵒᵈ), (CompleteLatticeHom.dual f).toFun a = OrderDual.toDual (f (OrderDual.ofDual a))

                                                      Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual lattices.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        @[simp]
                                                        theorem CompleteLatticeHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (g : CompleteLatticeHom β γ) (f : CompleteLatticeHom α β) :
                                                        CompleteLatticeHom.dual (g.comp f) = (CompleteLatticeHom.dual g).comp (CompleteLatticeHom.dual f)
                                                        @[simp]
                                                        theorem CompleteLatticeHom.symm_dual_id {α : Type u_2} [CompleteLattice α] :
                                                        CompleteLatticeHom.dual.symm (CompleteLatticeHom.id αᵒᵈ) = CompleteLatticeHom.id α
                                                        @[simp]
                                                        theorem CompleteLatticeHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (g : CompleteLatticeHom βᵒᵈ γᵒᵈ) (f : CompleteLatticeHom αᵒᵈ βᵒᵈ) :
                                                        CompleteLatticeHom.dual.symm (g.comp f) = (CompleteLatticeHom.dual.symm g).comp (CompleteLatticeHom.dual.symm f)

                                                        Concrete homs #

                                                        def CompleteLatticeHom.setPreimage {α : Type u_2} {β : Type u_3} (f : αβ) :

                                                        Set.preimage as a complete lattice homomorphism.

                                                        See also sSupHom.setImage.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem CompleteLatticeHom.coe_setPreimage {α : Type u_2} {β : Type u_3} (f : αβ) :
                                                          @[simp]
                                                          theorem CompleteLatticeHom.setPreimage_apply {α : Type u_2} {β : Type u_3} (f : αβ) (s : Set β) :
                                                          theorem CompleteLatticeHom.setPreimage_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : βγ) (f : αβ) :
                                                          theorem Set.image_sSup {α : Type u_2} {β : Type u_3} {f : αβ} (s : Set (Set α)) :
                                                          f '' sSup s = sSup (Set.image f '' s)
                                                          @[simp]
                                                          theorem sSupHom.setImage_toFun {α : Type u_2} {β : Type u_3} (f : αβ) (s : Set α) :
                                                          def sSupHom.setImage {α : Type u_2} {β : Type u_3} (f : αβ) :
                                                          sSupHom (Set α) (Set β)

                                                          Using Set.image, a function between types yields a sSupHom between their lattices of subsets.

                                                          See also CompleteLatticeHom.setPreimage.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem Equiv.toOrderIsoSet_apply {α : Type u_2} {β : Type u_3} (e : α β) (s : Set α) :
                                                            e.toOrderIsoSet s = e '' s
                                                            @[simp]
                                                            theorem Equiv.toOrderIsoSet_symm_apply {α : Type u_2} {β : Type u_3} (e : α β) (s : Set β) :
                                                            (RelIso.symm e.toOrderIsoSet) s = e.symm '' s
                                                            def Equiv.toOrderIsoSet {α : Type u_2} {β : Type u_3} (e : α β) :
                                                            Set α ≃o Set β

                                                            An equivalence of types yields an order isomorphism between their lattices of subsets.

                                                            Equations
                                                            • e.toOrderIsoSet = { toFun := fun (s : Set α) => e '' s, invFun := fun (s : Set β) => e.symm '' s, left_inv := , right_inv := , map_rel_iff' := }
                                                            Instances For
                                                              def supsSupHom {α : Type u_2} [CompleteLattice α] :
                                                              sSupHom (α × α) α

                                                              The map (a, b) ↦ a ⊔ b as a sSupHom.

                                                              Equations
                                                              • supsSupHom = { toFun := fun (x : α × α) => x.1 x.2, map_sSup' := }
                                                              Instances For
                                                                def infsInfHom {α : Type u_2} [CompleteLattice α] :
                                                                sInfHom (α × α) α

                                                                The map (a, b) ↦ a ⊓ b as an sInfHom.

                                                                Equations
                                                                • infsInfHom = { toFun := fun (x : α × α) => x.1 x.2, map_sInf' := }
                                                                Instances For
                                                                  @[simp]
                                                                  theorem supsSupHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) :
                                                                  supsSupHom x = x.1 x.2
                                                                  @[simp]
                                                                  theorem infsInfHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) :
                                                                  infsInfHom x = x.1 x.2