Documentation

Mathlib.Order.Heyting.Hom

Heyting algebra morphisms #

A Heyting homomorphism between two Heyting algebras is a bounded lattice homomorphism that preserves Heyting implication.

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 #

structure HeytingHom (α : Type u_6) (β : Type u_7) [HeytingAlgebra α] [HeytingAlgebra β] extends LatticeHom :
Type (max u_6 u_7)

The type of Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication.

  • toFun : αβ
  • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
  • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
  • map_bot' : self.toFun =

    The proposition that a Heyting homomorphism preserves the bottom element.

  • map_himp' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

    The proposition that a Heyting homomorphism preserves the Heyting implication.

Instances For
    theorem HeytingHom.map_bot' {α : Type u_6} {β : Type u_7} [HeytingAlgebra α] [HeytingAlgebra β] (self : HeytingHom α β) :
    self.toFun =

    The proposition that a Heyting homomorphism preserves the bottom element.

    theorem HeytingHom.map_himp' {α : Type u_6} {β : Type u_7} [HeytingAlgebra α] [HeytingAlgebra β] (self : HeytingHom α β) (a : α) (b : α) :
    self.toFun (a b) = self.toFun a self.toFun b

    The proposition that a Heyting homomorphism preserves the Heyting implication.

    structure CoheytingHom (α : Type u_6) (β : Type u_7) [CoheytingAlgebra α] [CoheytingAlgebra β] extends LatticeHom :
    Type (max u_6 u_7)

    The type of co-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve difference.

    • toFun : αβ
    • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
    • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
    • map_top' : self.toFun =

      The proposition that a co-Heyting homomorphism preserves the top element.

    • map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b

      The proposition that a co-Heyting homomorphism preserves the difference operation.

    Instances For
      theorem CoheytingHom.map_top' {α : Type u_6} {β : Type u_7} [CoheytingAlgebra α] [CoheytingAlgebra β] (self : CoheytingHom α β) :
      self.toFun =

      The proposition that a co-Heyting homomorphism preserves the top element.

      theorem CoheytingHom.map_sdiff' {α : Type u_6} {β : Type u_7} [CoheytingAlgebra α] [CoheytingAlgebra β] (self : CoheytingHom α β) (a : α) (b : α) :
      self.toFun (a \ b) = self.toFun a \ self.toFun b

      The proposition that a co-Heyting homomorphism preserves the difference operation.

      structure BiheytingHom (α : Type u_6) (β : Type u_7) [BiheytingAlgebra α] [BiheytingAlgebra β] extends LatticeHom :
      Type (max u_6 u_7)

      The type of bi-Heyting homomorphisms from α to β. Bounded lattice homomorphisms that preserve Heyting implication and difference.

      • toFun : αβ
      • map_sup' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
      • map_inf' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b
      • map_himp' : ∀ (a b : α), self.toFun (a b) = self.toFun a self.toFun b

        The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

      • map_sdiff' : ∀ (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b

        The proposition that a bi-Heyting homomorphism preserves the difference operation.

      Instances For
        theorem BiheytingHom.map_himp' {α : Type u_6} {β : Type u_7} [BiheytingAlgebra α] [BiheytingAlgebra β] (self : BiheytingHom α β) (a : α) (b : α) :
        self.toFun (a b) = self.toFun a self.toFun b

        The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

        theorem BiheytingHom.map_sdiff' {α : Type u_6} {β : Type u_7} [BiheytingAlgebra α] [BiheytingAlgebra β] (self : BiheytingHom α β) (a : α) (b : α) :
        self.toFun (a \ b) = self.toFun a \ self.toFun b

        The proposition that a bi-Heyting homomorphism preserves the difference operation.

        class HeytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

        HeytingHomClass F α β states that F is a type of Heyting homomorphisms.

        You should extend this class when you extend HeytingHom.

        • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
        • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
        • map_bot : ∀ (f : F), f =

          The proposition that a Heyting homomorphism preserves the bottom element.

        • map_himp : ∀ (f : F) (a b : α), f (a b) = f a f b

          The proposition that a Heyting homomorphism preserves the Heyting implication.

        Instances
          theorem HeytingHomClass.map_bot {F : Type u_6} {α : Type u_7} {β : Type u_8} [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] [self : HeytingHomClass F α β] (f : F) :

          The proposition that a Heyting homomorphism preserves the bottom element.

          @[simp]
          theorem HeytingHomClass.map_himp {F : Type u_6} {α : Type u_7} {β : Type u_8} [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] [self : HeytingHomClass F α β] (f : F) (a : α) (b : α) :
          f (a b) = f a f b

          The proposition that a Heyting homomorphism preserves the Heyting implication.

          class CoheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [CoheytingAlgebra α] [CoheytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

          CoheytingHomClass F α β states that F is a type of co-Heyting homomorphisms.

          You should extend this class when you extend CoheytingHom.

          • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
          • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
          • map_top : ∀ (f : F), f =

            The proposition that a co-Heyting homomorphism preserves the top element.

          • map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b

            The proposition that a co-Heyting homomorphism preserves the difference operation.

          Instances
            theorem CoheytingHomClass.map_top {F : Type u_6} {α : Type u_7} {β : Type u_8} [CoheytingAlgebra α] [CoheytingAlgebra β] [FunLike F α β] [self : CoheytingHomClass F α β] (f : F) :

            The proposition that a co-Heyting homomorphism preserves the top element.

            @[simp]
            theorem CoheytingHomClass.map_sdiff {F : Type u_6} {α : Type u_7} {β : Type u_8} [CoheytingAlgebra α] [CoheytingAlgebra β] [FunLike F α β] [self : CoheytingHomClass F α β] (f : F) (a : α) (b : α) :
            f (a \ b) = f a \ f b

            The proposition that a co-Heyting homomorphism preserves the difference operation.

            class BiheytingHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] extends LatticeHomClass :

            BiheytingHomClass F α β states that F is a type of bi-Heyting homomorphisms.

            You should extend this class when you extend BiheytingHom.

            • map_sup : ∀ (f : F) (a b : α), f (a b) = f a f b
            • map_inf : ∀ (f : F) (a b : α), f (a b) = f a f b
            • map_himp : ∀ (f : F) (a b : α), f (a b) = f a f b

              The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

            • map_sdiff : ∀ (f : F) (a b : α), f (a \ b) = f a \ f b

              The proposition that a bi-Heyting homomorphism preserves the difference operation.

            Instances
              theorem BiheytingHomClass.map_himp {F : Type u_6} {α : Type u_7} {β : Type u_8} [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] [self : BiheytingHomClass F α β] (f : F) (a : α) (b : α) :
              f (a b) = f a f b

              The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

              theorem BiheytingHomClass.map_sdiff {F : Type u_6} {α : Type u_7} {β : Type u_8} [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] [self : BiheytingHomClass F α β] (f : F) (a : α) (b : α) :
              f (a \ b) = f a \ f b

              The proposition that a bi-Heyting homomorphism preserves the difference operation.

              @[instance 100]
              instance HeytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] :
              ∀ {x : HeytingAlgebra β} [inst : HeytingHomClass F α β], BoundedLatticeHomClass F α β
              Equations
              • =
              @[instance 100]
              instance CoheytingHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] :
              ∀ {x : CoheytingAlgebra β} [inst : CoheytingHomClass F α β], BoundedLatticeHomClass F α β
              Equations
              • =
              @[instance 100]
              instance BiheytingHomClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] :
              ∀ {x : BiheytingAlgebra β} [inst : BiheytingHomClass F α β], HeytingHomClass F α β
              Equations
              • =
              @[instance 100]
              instance BiheytingHomClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] :
              ∀ {x : BiheytingAlgebra β} [inst : BiheytingHomClass F α β], CoheytingHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [HeytingAlgebra α] :
              ∀ {x : HeytingAlgebra β} [inst : OrderIsoClass F α β], HeytingHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [CoheytingAlgebra α] :
              ∀ {x : CoheytingAlgebra β} [inst : OrderIsoClass F α β], CoheytingHomClass F α β
              Equations
              • =
              @[instance 100]
              instance OrderIsoClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [BiheytingAlgebra α] :
              ∀ {x : BiheytingAlgebra β} [inst : OrderIsoClass F α β], BiheytingHomClass F α β
              Equations
              • =
              theorem BoundedLatticeHomClass.toBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BooleanAlgebra α] [BooleanAlgebra β] [BoundedLatticeHomClass F α β] :

              This can't be an instance because of typeclass loops.

              @[simp]
              theorem map_compl {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α) :
              f a = (f a)
              @[simp]
              theorem map_bihimp {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α) (b : α) :
              f (bihimp a b) = bihimp (f a) (f b)
              @[simp]
              theorem map_hnot {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α) :
              f (a) = f a
              @[simp]
              theorem map_symmDiff {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a : α) (b : α) :
              f (symmDiff a b) = symmDiff (f a) (f b)
              instance instCoeTCHeytingHomOfHeytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [HeytingAlgebra α] [HeytingAlgebra β] [HeytingHomClass F α β] :
              CoeTC F (HeytingHom α β)
              Equations
              • instCoeTCHeytingHomOfHeytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_bot' := , map_himp' := } }
              instance instCoeTCCoheytingHomOfCoheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingHomClass F α β] :
              Equations
              • instCoeTCCoheytingHomOfCoheytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_top' := , map_sdiff' := } }
              instance instCoeTCBiheytingHomOfBiheytingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingHomClass F α β] :
              Equations
              • instCoeTCBiheytingHomOfBiheytingHomClass = { coe := fun (f : F) => { toFun := f, map_sup' := , map_inf' := , map_himp' := , map_sdiff' := } }
              instance HeytingHom.instFunLike {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :
              FunLike (HeytingHom α β) α β
              Equations
              • HeytingHom.instFunLike = { coe := fun (f : HeytingHom α β) => f.toFun, coe_injective' := }
              instance HeytingHom.instHeytingHomClass {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] :
              Equations
              • =
              theorem HeytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} :
              f.toFun = f
              @[simp]
              theorem HeytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} :
              f.toLatticeHom = f
              theorem HeytingHom.ext {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] {f : HeytingHom α β} {g : HeytingHom α β} (h : ∀ (a : α), f a = g a) :
              f = g
              def HeytingHom.copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : αβ) (h : f' = f) :

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

              Equations
              • f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_bot' := , map_himp' := }
              Instances For
                @[simp]
                theorem HeytingHom.coe_copy {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : αβ) (h : f' = f) :
                (f.copy f' h) = f'
                theorem HeytingHom.copy_eq {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) (f' : αβ) (h : f' = f) :
                f.copy f' h = f
                def HeytingHom.id (α : Type u_2) [HeytingAlgebra α] :

                id as a HeytingHom.

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

                  Composition of HeytingHoms as a HeytingHom.

                  Equations
                  • f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_bot' := , map_himp' := }
                  Instances For
                    @[simp]
                    theorem HeytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) :
                    (f.comp g) = f g
                    @[simp]
                    theorem HeytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] (f : HeytingHom β γ) (g : HeytingHom α β) (a : α) :
                    (f.comp g) a = f (g a)
                    @[simp]
                    theorem HeytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] [HeytingAlgebra δ] (f : HeytingHom γ δ) (g : HeytingHom β γ) (h : HeytingHom α β) :
                    (f.comp g).comp h = f.comp (g.comp h)
                    @[simp]
                    theorem HeytingHom.comp_id {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) :
                    f.comp (HeytingHom.id α) = f
                    @[simp]
                    theorem HeytingHom.id_comp {α : Type u_2} {β : Type u_3} [HeytingAlgebra α] [HeytingAlgebra β] (f : HeytingHom α β) :
                    (HeytingHom.id β).comp f = f
                    @[simp]
                    theorem HeytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f : HeytingHom α β} {g₁ : HeytingHom β γ} {g₂ : HeytingHom β γ} (hf : Function.Surjective f) :
                    g₁.comp f = g₂.comp f g₁ = g₂
                    @[simp]
                    theorem HeytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] {f₁ : HeytingHom α β} {f₂ : HeytingHom α β} {g : HeytingHom β γ} (hg : Function.Injective g) :
                    g.comp f₁ = g.comp f₂ f₁ = f₂
                    instance CoheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] :
                    FunLike (CoheytingHom α β) α β
                    Equations
                    • CoheytingHom.instFunLike = { coe := fun (f : CoheytingHom α β) => f.toFun, coe_injective' := }
                    Equations
                    • =
                    theorem CoheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} :
                    f.toFun = f
                    @[simp]
                    theorem CoheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} :
                    f.toLatticeHom = f
                    theorem CoheytingHom.ext {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] {f : CoheytingHom α β} {g : CoheytingHom α β} (h : ∀ (a : α), f a = g a) :
                    f = g
                    def CoheytingHom.copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : αβ) (h : f' = f) :

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

                    Equations
                    • f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_top' := , map_sdiff' := }
                    Instances For
                      @[simp]
                      theorem CoheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : αβ) (h : f' = f) :
                      (f.copy f' h) = f'
                      theorem CoheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) (f' : αβ) (h : f' = f) :
                      f.copy f' h = f

                      id as a CoheytingHom.

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

                        Composition of CoheytingHoms as a CoheytingHom.

                        Equations
                        • f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_top' := , map_sdiff' := }
                        Instances For
                          @[simp]
                          theorem CoheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) :
                          (f.comp g) = f g
                          @[simp]
                          theorem CoheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] (f : CoheytingHom β γ) (g : CoheytingHom α β) (a : α) :
                          (f.comp g) a = f (g a)
                          @[simp]
                          theorem CoheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] [CoheytingAlgebra δ] (f : CoheytingHom γ δ) (g : CoheytingHom β γ) (h : CoheytingHom α β) :
                          (f.comp g).comp h = f.comp (g.comp h)
                          @[simp]
                          theorem CoheytingHom.comp_id {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) :
                          f.comp (CoheytingHom.id α) = f
                          @[simp]
                          theorem CoheytingHom.id_comp {α : Type u_2} {β : Type u_3} [CoheytingAlgebra α] [CoheytingAlgebra β] (f : CoheytingHom α β) :
                          (CoheytingHom.id β).comp f = f
                          @[simp]
                          theorem CoheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f : CoheytingHom α β} {g₁ : CoheytingHom β γ} {g₂ : CoheytingHom β γ} (hf : Function.Surjective f) :
                          g₁.comp f = g₂.comp f g₁ = g₂
                          @[simp]
                          theorem CoheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CoheytingAlgebra α] [CoheytingAlgebra β] [CoheytingAlgebra γ] {f₁ : CoheytingHom α β} {f₂ : CoheytingHom α β} {g : CoheytingHom β γ} (hg : Function.Injective g) :
                          g.comp f₁ = g.comp f₂ f₁ = f₂
                          instance BiheytingHom.instFunLike {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] :
                          FunLike (BiheytingHom α β) α β
                          Equations
                          • BiheytingHom.instFunLike = { coe := fun (f : BiheytingHom α β) => f.toFun, coe_injective' := }
                          Equations
                          • =
                          theorem BiheytingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} :
                          f.toFun = f
                          @[simp]
                          theorem BiheytingHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} :
                          f.toLatticeHom = f
                          theorem BiheytingHom.ext {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] {f : BiheytingHom α β} {g : BiheytingHom α β} (h : ∀ (a : α), f a = g a) :
                          f = g
                          def BiheytingHom.copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : αβ) (h : f' = f) :

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

                          Equations
                          • f.copy f' h = { toFun := f', map_sup' := , map_inf' := , map_himp' := , map_sdiff' := }
                          Instances For
                            @[simp]
                            theorem BiheytingHom.coe_copy {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : αβ) (h : f' = f) :
                            (f.copy f' h) = f'
                            theorem BiheytingHom.copy_eq {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) (f' : αβ) (h : f' = f) :
                            f.copy f' h = f

                            id as a BiheytingHom.

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

                              Composition of BiheytingHoms as a BiheytingHom.

                              Equations
                              • f.comp g = let __src := f.comp g.toLatticeHom; { toFun := f g, map_sup' := , map_inf' := , map_himp' := , map_sdiff' := }
                              Instances For
                                @[simp]
                                theorem BiheytingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) :
                                (f.comp g) = f g
                                @[simp]
                                theorem BiheytingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β) (a : α) :
                                (f.comp g) a = f (g a)
                                @[simp]
                                theorem BiheytingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] [BiheytingAlgebra δ] (f : BiheytingHom γ δ) (g : BiheytingHom β γ) (h : BiheytingHom α β) :
                                (f.comp g).comp h = f.comp (g.comp h)
                                @[simp]
                                theorem BiheytingHom.comp_id {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) :
                                f.comp (BiheytingHom.id α) = f
                                @[simp]
                                theorem BiheytingHom.id_comp {α : Type u_2} {β : Type u_3} [BiheytingAlgebra α] [BiheytingAlgebra β] (f : BiheytingHom α β) :
                                (BiheytingHom.id β).comp f = f
                                @[simp]
                                theorem BiheytingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f : BiheytingHom α β} {g₁ : BiheytingHom β γ} {g₂ : BiheytingHom β γ} (hf : Function.Surjective f) :
                                g₁.comp f = g₂.comp f g₁ = g₂
                                @[simp]
                                theorem BiheytingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BiheytingAlgebra α] [BiheytingAlgebra β] [BiheytingAlgebra γ] {f₁ : BiheytingHom α β} {f₂ : BiheytingHom α β} {g : BiheytingHom β γ} (hg : Function.Injective g) :
                                g.comp f₁ = g.comp f₂ f₁ = f₂