Documentation

Linglib.Core.Data.Setoid.Basic

Kernel monotonicity, meets, and decidable equality for setoids #

This file adds to Mathlib/Data/Setoid/Basic.lean the monotonicity of Setoid.ker under composition and its equality case for an injective outer map, the relation of an indexed meet of setoids, the classes of a meet and the order in terms of classes, and decidable equality of setoids on a finite type. Mathlib has the monotonicity for algebraic kernels (LinearMap.ker_le_ker_comp, MonoidHom.comap_ker, RingHom.ker_comp_of_injective) but not for the plain Setoid.ker they specialize. [UPSTREAM]

source
theorem Setoid.ker_le_ker_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (h : β → γ) :
ker f ≤ ker (h ∘ f)

If g factors through f, then the kernel of f refines the kernel of g — the Setoid primitive of LinearMap.ker_le_ker_comp. [UPSTREAM]

source
theorem Setoid.ker_comp_of_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) {g : β → γ} (hg : Function.Injective g) :
ker (g ∘ f) = ker f

The kernel of a map followed by an injection is the kernel of the map, the Setoid primitive of RingHom.ker_comp_of_injective. [UPSTREAM]

source
theorem Setoid.iInf_iff {α : Type u_1} {ι : Sort u_2} {f : ι → Setoid α} {a b : α} :
(⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i) a b

Two elements are related by an indexed meet of setoids when every setoid relates them. [UPSTREAM]

source
theorem Setoid.classes_inf {α : Type u_1} (r s : Setoid α) :
(r ⊓ s).classes = {c : Set α | ∃ a ∈ r.classes, ∃ b ∈ s.classes, c = a ∩ b ∧ c.Nonempty}

The classes of a meet of setoids are the nonempty intersections of their classes. [UPSTREAM]

source
theorem Setoid.le_iff_forall_classes {α : Type u_1} {r s : Setoid α} :
r ≤ s ↔ ∀ a ∈ r.classes, ∃ b ∈ s.classes, a ⊆ b

One setoid is finer than another when each of its classes lies in a class of the other. [UPSTREAM]

source
@[instance_reducible]
instance Setoid.ker.decidableRel {α : Type u_1} {β : Type u_2} (f : α → β) [DecidableEq β] :
DecidableRel ⇑(ker f)

The kernel of a map into a type with decidable equality is decidable. [UPSTREAM]

Equations
source
@[instance_reducible]
instance Setoid.decidableEqOfDecidableRel {α : Type u_1} [Fintype α] (s t : Setoid α) [DecidableRel ⇑s] [DecidableRel ⇑t] :
Decidable (s = t)

Equality of setoids on a finite type is decided pairwise. [UPSTREAM]

Equations