Mathlib.Control.ULift

PLift.map definition

(f : α → β) (a : PLift α) : PLift β

Full source

/-- Functorial action. -/
protected def map (f : α → β) (a : PLift α) : PLift β :=
  PLift.up (f a.down)

Lifted function application

Informal description

Given a function $f : \alpha \to \beta$ and a lifted element $a : \text{PLift} \alpha$, the function $\text{PLift.map}$ applies $f$ to the underlying value of $a$ and returns the result as a lifted element in $\text{PLift} \beta$. Specifically, if $a = \text{PLift.up} x$ for some $x \in \alpha$, then $\text{PLift.map} f a = \text{PLift.up} (f x)$.

PLift.map_up theorem

(f : α → β) (a : α) : (PLift.up a).map f = PLift.up (f a)

Full source

@[simp]
theorem map_up (f : α → β) (a : α) : (PLift.up a).map f = PLift.up (f a) :=
  rfl

Lifted Function Application on Lifted Elements: $(\text{up}\, a).\text{map}\, f = \text{up}\, (f a)$

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, applying the lifted function $\text{PLift.map}\, f$ to the lifted element $\text{PLift.up}\, a$ results in $\text{PLift.up}\, (f a)$. In other words, $(\text{PLift.up}\, a).\text{map}\, f = \text{PLift.up}\, (f a)$.

PLift.pure definition

: α → PLift α

Full source

/-- Embedding of pure values. -/
@[simp]
protected def pure : α → PLift α :=
  up

Lifting pure values to PLift

Informal description

The function lifts a pure value of type $\alpha$ to a value of type $\text{PLift}\, \alpha$ by applying the constructor $\text{up}$.

PLift.seq definition

(f : PLift (α → β)) (x : Unit → PLift α) : PLift β

Full source

/-- Applicative sequencing. -/
protected def seq (f : PLift (α → β)) (x : Unit → PLift α) : PLift β :=
  PLift.up (f.down (x ()).down)

Sequencing operation for lifted functions

Informal description

Given a lifted function `f : PLift (α → β)` and a thunk `x : Unit → PLift α`, the sequencing operation produces a lifted value in `PLift β` by applying the function inside `f` to the value inside the result of evaluating `x ()`.

PLift.seq_up theorem

(f : α → β) (x : α) : (PLift.up f).seq (fun _ => PLift.up x) = PLift.up (f x)

Full source

@[simp]
theorem seq_up (f : α → β) (x : α) : (PLift.up f).seq (fun _ => PLift.up x) = PLift.up (f x) :=
  rfl

Sequencing of Lifted Function and Value Yields Lifted Result

Informal description

For any function $f : \alpha \to \beta$ and any element $x : \alpha$, the sequencing operation applied to the lifted function $\text{PLift.up}\, f$ and the thunk returning $\text{PLift.up}\, x$ yields $\text{PLift.up}\, (f x)$. That is, $(\text{PLift.up}\, f).\text{seq} (\lambda \_. \text{PLift.up}\, x) = \text{PLift.up}\, (f x)$.

PLift.bind definition

(a : PLift α) (f : α → PLift β) : PLift β

Full source

/-- Monadic bind. -/
protected def bind (a : PLift α) (f : α → PLift β) : PLift β :=
  f a.down

Monadic bind for `PLift`

Informal description

The monadic bind operation for `PLift`, which takes a lifted value `a : PLift α` and a function `f : α → PLift β`, and returns the result of applying `f` to the underlying value of `a`.

PLift.bind_up theorem

(a : α) (f : α → PLift β) : (PLift.up a).bind f = f a

Full source

@[simp]
theorem bind_up (a : α) (f : α → PLift β) : (PLift.up a).bind f = f a :=
  rfl

Monadic Bind Property for Lifted Values: $(\text{up}(a)).\text{bind}(f) = f(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $f \colon \alpha \to \text{PLift} \beta$, the monadic bind operation applied to the lifted value $\text{PLift.up}(a)$ and the function $f$ is equal to $f(a)$.

PLift.instMonad_mathlib instance

: Monad PLift

Full source

instance : Monad PLift where
  map := @PLift.map
  pure := @PLift.pure
  seq := @PLift.seq
  bind := @PLift.bind

Monad instance for PLift

Informal description

The type constructor `PLift` forms a monad, where: - The pure operation lifts a value of type $\alpha$ to `PLift α` - The bind operation takes a lifted value `a : PLift α` and a function `f : α → PLift β`, and applies `f` to the underlying value of `a`

PLift.instLawfulFunctor_mathlib instance

: LawfulFunctor PLift

Full source

instance : LawfulFunctor PLift where
  id_map := @fun _ ⟨_⟩ => rfl
  comp_map := @fun _ _ _ _ _ ⟨_⟩ => rfl
  map_const := @fun _ _ => rfl

`PLift` is a Lawful Functor

Informal description

The type constructor `PLift` forms a lawful functor, meaning it satisfies the functor laws with respect to its map operation.

PLift.instLawfulApplicative_mathlib instance

: LawfulApplicative PLift

Full source

instance : LawfulApplicative PLift where
  seqLeft_eq := @fun _ _ _ _ => rfl
  seqRight_eq := @fun _ _ _ _ => rfl
  pure_seq := @fun _ _ _ ⟨_⟩ => rfl
  map_pure := @fun _ _ _ _ => rfl
  seq_pure := @fun _ _ ⟨_⟩ _ => rfl
  seq_assoc := @fun _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩ => rfl

`PLift` is a Lawful Applicative Functor

Informal description

The type constructor `PLift` forms a lawful applicative functor, meaning it satisfies the applicative functor laws with respect to its pure and seq operations.

PLift.instLawfulMonad_mathlib instance

: LawfulMonad PLift

Full source

instance : LawfulMonad PLift where
  bind_pure_comp := @fun _ _ _ ⟨_⟩ => rfl
  bind_map := @fun _ _ ⟨_⟩ ⟨_⟩ => rfl
  pure_bind := @fun _ _ _ _ => rfl
  bind_assoc := @fun _ _ _ ⟨_⟩ _ _ => rfl

`PLift` is a Lawful Monad

Informal description

The type constructor `PLift` forms a lawful monad, meaning it satisfies the monad laws with respect to its pure and bind operations.

PLift.rec.constant theorem

{α : Sort u} {β : Type v} (b : β) : (@PLift.rec α (fun _ => β) fun _ => b) = fun _ => b

Full source

@[simp]
theorem rec.constant {α : Sort u} {β : Type v} (b : β) :
    (@PLift.rec α (fun _ => β) fun _ => b) = fun _ => b := rfl

Constant Function Recursion Principle for `PLift`

Informal description

For any type `α` and any type `β`, given a constant function `fun _ => b` where `b : β`, the recursion principle `PLift.rec` applied to this function is equal to the constant function `fun _ => b`.

ULift.map definition

(f : α → β) (a : ULift.{u'} α) : ULift.{v'} β

Full source

/-- Functorial action. -/
protected def map (f : α → β) (a : ULift.{u'} α) : ULift.{v'} β := ULift.up.{v'} (f a.down)

Mapping a function over a universe-lifted value

Informal description

The function applies a given function $ f : \alpha \to \beta $ to the underlying value of a universe-lifted type $ \text{ULift}\, \alpha $, and returns the result wrapped in $ \text{ULift}\, \beta $.

ULift.map_up theorem

(f : α → β) (a : α) : (ULift.up.{u'} a).map f = ULift.up.{v'} (f a)

Full source

@[simp]
theorem map_up (f : α → β) (a : α) : (ULift.up.{u'} a).map f = ULift.up.{v'} (f a) := rfl

Mapping a Function over a Lifted Element Preserves the Lift

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, applying the lifted function $\text{ULift.map}\, f$ to the lifted element $\text{ULift.up}\, a$ results in the lifted value $\text{ULift.up}\, (f a)$.

ULift.pure definition

: α → ULift α

Full source

/-- Embedding of pure values. -/
@[simp]
protected def pure : α → ULift α :=
  up

Lifting a value to a universe-lifted type

Informal description

The function lifts a value of type $\alpha$ to the universe-lifted type $\text{ULift}\, \alpha$ by wrapping it in the $\text{ULift.up}$ constructor.

ULift.seq definition

{α β} (f : ULift (α → β)) (x : Unit → ULift α) : ULift β

Full source

/-- Applicative sequencing. -/
protected def seq {α β} (f : ULift (α → β)) (x : Unit → ULift α) : ULift β :=
  ULift.up.{u} (f.down (x ()).down)

Sequential application for lifted types

Informal description

The sequential application operation for `ULift`, which takes a lifted function `f : ULift (α → β)` and a thunk `x : Unit → ULift α`, and returns the result of applying the underlying function of `f` to the underlying value of `x ()`, lifted back to `ULift β`.

ULift.seq_up theorem

(f : α → β) (x : α) : (ULift.up f).seq (fun _ => ULift.up x) = ULift.up (f x)

Full source

@[simp]
theorem seq_up (f : α → β) (x : α) : (ULift.up f).seq (fun _ => ULift.up x) = ULift.up (f x) :=
  rfl

Sequential Application Property for Lifted Functions: $(\text{up}(f)) \mathbin{\text{seq}} (\lambda \_. \text{up}(x)) = \text{up}(f(x))$

Informal description

For any function $f : \alpha \to \beta$ and any element $x \in \alpha$, the sequential application of the lifted function $\text{up}(f)$ to the thunk returning $\text{up}(x)$ equals the lifted result $\text{up}(f(x))$.

ULift.bind definition

(a : ULift α) (f : α → ULift β) : ULift β

Full source

/-- Monadic bind. -/
protected def bind (a : ULift α) (f : α → ULift β) : ULift β :=
  f a.down

Monadic bind for lifted types

Informal description

The monadic bind operation for `ULift`, which takes a lifted value `a : ULift α` and a function `f : α → ULift β`, and returns the result of applying `f` to the underlying value of `a`.

ULift.bind_up theorem

(a : α) (f : α → ULift β) : (ULift.up a).bind f = f a

Full source

@[simp]
theorem bind_up (a : α) (f : α → ULift β) : (ULift.up a).bind f = f a :=
  rfl

Monadic Bind Property for Lifted Values: $(\text{up}(a)).\text{bind} f = f(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $f : \alpha \to \text{ULift} \beta$, the monadic bind operation applied to the lifted value $\text{ULift.up}(a)$ and the function $f$ is equal to $f(a)$.

ULift.instMonad_mathlib instance

: Monad ULift

Full source

instance : Monad ULift where
  map := @ULift.map
  pure := @ULift.pure
  seq := @ULift.seq
  bind := @ULift.bind

Monad Structure on Universe-Lifted Types

Informal description

The universe-lifted type `ULift α` has a monad structure, where: - The pure operation lifts a value `a : α` to `ULift.up a` - The bind operation applies a function `f : α → ULift β` to the underlying value of a lifted term

ULift.instLawfulFunctor_mathlib instance

: LawfulFunctor ULift

Full source

instance : LawfulFunctor ULift where
  id_map := @fun _ ⟨_⟩ => rfl
  comp_map := @fun _ _ _ _ _ ⟨_⟩ => rfl
  map_const := @fun _ _ => rfl

Lawful Functor Structure on Universe-Lifted Types

Informal description

The universe-lifted type `ULift α` satisfies the functor laws, meaning that its `map` operation preserves identity and composition of functions.

ULift.instLawfulApplicative_mathlib instance

: LawfulApplicative ULift

Full source

instance : LawfulApplicative ULift where
  seqLeft_eq := @fun _ _ _ _ => rfl
  seqRight_eq := @fun _ _ _ _ => rfl
  pure_seq := @fun _ _ _ ⟨_⟩ => rfl
  map_pure := @fun _ _ _ _ => rfl
  seq_pure := @fun _ _ ⟨_⟩ _ => rfl
  seq_assoc := @fun _ _ _ ⟨_⟩ ⟨_⟩ ⟨_⟩ => rfl

Lawful Applicative Structure on Universe-Lifted Types

Informal description

The universe-lifted type `ULift α` satisfies the applicative functor laws, meaning its operations preserve identity and composition of functions while maintaining the relationship between `pure` and `<*>`.

ULift.instLawfulMonad_mathlib instance

: LawfulMonad ULift

Full source

instance : LawfulMonad ULift where
  bind_pure_comp := @fun _ _ _ ⟨_⟩ => rfl
  bind_map := @fun _ _ ⟨_⟩ ⟨_⟩ => rfl
  pure_bind := @fun _ _ _ _ => rfl
  bind_assoc := @fun _ _ _ ⟨_⟩ _ _ => rfl

Lawful Monad Structure on Universe-Lifted Types

Informal description

The universe-lifted type `ULift α` satisfies the monad laws, meaning its operations preserve identity and composition of functions while maintaining the relationship between `pure` and `>>=`.

ULift.rec.constant theorem

{α : Type u} {β : Sort v} (b : β) : (@ULift.rec α (fun _ => β) fun _ => b) = fun _ => b

Full source

@[simp]
theorem rec.constant {α : Type u} {β : Sort v} (b : β) :
    (@ULift.rec α (fun _ => β) fun _ => b) = fun _ => b := rfl

Constant Recursion Principle for ULift

Informal description

For any type `α` and any sort `β`, given a constant value `b : β`, the recursive elimination principle `ULift.rec` applied to the constant function `(fun _ => b)` is equal to the constant function `(fun _ => b)` itself. In other words, `ULift.rec (fun _ => b) = (fun _ => b)`.