Transfer order structures across equivs

In this file we prove theorems of the following form: if β has a group structure and α ≃ β then α has a group structure, and similarly for monoids, semigroups, rings, integral domains, fields and so on.

Note that most of these constructions can also be obtained using the transport tactic.

Tags

equiv

def Equiv.hasLe {α : Type u_1} {β : Type u_2} (e : α ≃ β) [LE β] : LE α

Transfer has_le across an equiv

Equations

• e.hasLe = { le := fun (x y : α) => e x ≤ e y }

def Equiv.hasLt {α : Type u_1} {β : Type u_2} (e : α ≃ β) [LT β] : LT α

Transfer has_lt across an equiv

Equations

• e.hasLt = { lt := fun (x y : α) => e x < e y }

def Equiv.hasTop {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Top β] : Top α

Transfer has_top across an equiv

Equations

• e.hasTop = { top := e.symm ⊤ }

def Equiv.hasBot {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Bot β] : Bot α

Transfer has_bot across an equiv

Equations

• e.hasBot = { bot := e.symm ⊥ }

def Equiv.hasSup {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Sup β] : Sup α

Transfer has_sup across an equiv

Equations

• e.hasSup = { sup := fun (x y : α) => e.symm (e x ⊔ e y) }

def Equiv.hasInf {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Inf β] : Inf α

Transfer has_inf across an equiv

Equations

• e.hasInf = { inf := fun (x y : α) => e.symm (e x ⊓ e y) }

def Equiv.hasSupSet {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SupSet β] : SupSet α

Transfer has_Sup across an equiv

Equations

• e.hasSupSet = { sSup := fun (s : Set α) => e.symm (⨆ x ∈ s, e x) }

def Equiv.hasInfSet {α : Type u_1} {β : Type u_2} (e : α ≃ β) [InfSet β] : InfSet α

Transfer has_Inf across an equiv

Equations

• e.hasInfSet = { sInf := fun (s : Set α) => e.symm (⨅ x ∈ s, e x) }

theorem Equiv.le_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [LE β] {x : α} {y : α} : x ≤ y ↔ e x ≤ e y

theorem Equiv.lt_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [LT β] {x : α} {y : α} : x < y ↔ e x < e y

theorem Equiv.top_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [Top β] : ⊤ = e.symm ⊤

theorem Equiv.bot_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [Bot β] : ⊥ = e.symm ⊥

theorem Equiv.sup_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [Sup β] (x : α) (y : α) : x ⊔ y = e.symm (e x ⊔ e y)

theorem Equiv.inf_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [Inf β] (x : α) (y : α) : x ⊓ y = e.symm (e x ⊓ e y)

theorem Equiv.sSup_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [SupSet β] (s : Set α) : sSup s = e.symm (⨆ x ∈ s, e x)

theorem Equiv.sInf_def {α : Type u_2} {β : Type u_1} (e : α ≃ β) [InfSet β] (s : Set α) : sInf s = e.symm (⨅ x ∈ s, e x)

def Equiv.orderIso {α : Type u_1} {β : Type u_2} (e : α ≃ β) [LE β] : α ≃o β

An equivalence e : α ≃ β gives a suptiplicative equivalence α ≃⊔ β where the suptiplicative structure on α is the top obtained by transporting a suptiplicative structure on β back along e.

Equations

• e.orderIso = { toEquiv := e, map_rel_iff' := ⋯ }

@[simp]

theorem Equiv.orderIso_apply {α : Type u_2} {β : Type u_1} (e : α ≃ β) [LE β] (a : α) : e.orderIso a = e a

theorem Equiv.orderIso_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) [LE β] (b : β) : e.orderIso.symm b = e.symm b

def Equiv.preorder {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Preorder β] : Preorder α

Transfer preorder across an equiv

Equations

• e.preorder = Preorder.lift ⇑e

def Equiv.partialOrder {α : Type u_1} {β : Type u_2} (e : α ≃ β) [PartialOrder β] : PartialOrder α

Transfer partial_order across an equiv

Equations

• e.partialOrder = PartialOrder.lift ⇑e ⋯

def Equiv.linearOrder {α : Type u_1} {β : Type u_2} (e : α ≃ β) [LinearOrder β] : LinearOrder α

Transfer linear_order across an equiv

Equations

• e.linearOrder = LinearOrder.lift' ⇑e ⋯

def Equiv.semilatticeSup {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SemilatticeSup β] : SemilatticeSup α

Transfer semilattice_sup across an equiv

Equations

• e.semilatticeSup = let sup := e.hasSup; Function.Injective.semilatticeSup ⇑e ⋯ ⋯

def Equiv.semilatticeInf {α : Type u_1} {β : Type u_2} (e : α ≃ β) [SemilatticeInf β] : SemilatticeInf α

Transfer semilattice_inf across an equiv

Equations

• e.semilatticeInf = let inf := e.hasInf; Function.Injective.semilatticeInf ⇑e ⋯ ⋯

def Equiv.lattice {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Lattice β] : Lattice α

Transfer lattice across an equiv

Equations

• e.lattice = let sup := e.hasSup; let inf := e.hasInf; Function.Injective.lattice ⇑e ⋯ ⋯ ⋯

def Equiv.completeLattice {α : Type u_1} {β : Type u_2} (e : α ≃ β) [CompleteLattice β] : CompleteLattice α

Transfer complete_lattice across an equiv

Equations

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

def Equiv.completeDistribLattice {α : Type u_1} {β : Type u_2} (e : α ≃ β) [CompleteDistribLattice β] : CompleteDistribLattice α

Transfer complete_distrib_lattice across an equiv

Equations

• e.completeDistribLattice = let completeLattice := e.completeLattice; Function.Injective.completeDistribLattice ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯