Theorems · Definition · combinatorics

Matroid.comap

{α : Type u_1} → {β : Type u_2} → Matroid β → (α → β) → Matroid α

The pullback of a matroid on β by a function f : α → β to a matroid on α. Elements with the same (nonloop) image are parallel and the ground set is f ⁻¹' M.E. The matroids M.comap f and M ↾ range f have isomorphic simplifications; the preimage of each nonloop of M ↾ range f is a parallel class.

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

24 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound