[Merged by Bors] - feat(Data/Matroid/Circuit): matroid cocircuits by apnelson1 · Pull Request #21692 · leanprover-community/mathlib4

apnelson1 · 2025-02-10T21:59:18Z

We add API for matroid cocircuits, including fundamental cocircuits and their relation to fundamental circuits.

depends on: [Merged by Bors] - feat(Matroid): cardinality criteria for indep/spanning sets to be bases #21512

Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>

github-actions · 2025-02-10T22:00:17Z

PR summary cffe782236

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Circuit.isCocircuit
+ Indep.exists_isCocircuit_inter_eq_mem
+ IsBase.compl_closure_diff_singleton_isCocircuit
+ IsBase.exchange_base_of_not_mem_closure
+ IsBase.mem_fundCocircuit_iff_mem_fundCircuit
+ IsCircuit.dual_rankPos
+ IsCircuit.inter_isCocircuit_ne_singleton
+ IsCircuit.isCocircuit_disjoint_or_nontrivial_inter
+ IsCircuit.isCocircuit_inter_nontrivial
+ IsCocircuit
+ IsCocircuit.circuit
+ IsCocircuit.subset_ground
+ coindep_iff_forall_subset_not_isCocircuit
+ dual_isCocircuit_iff
+ dual_rankPos_iff_exists_circuit
+ exists_circuit
+ fundCocircuit
+ fundCocircuit_eq_of_not_mem
+ fundCocircuit_eq_of_not_mem_ground
+ fundCocircuit_inter_eq
+ fundCocircuit_isCocircuit
+ fundCocircuit_subset_insert_compl
+ isCocircuit_def
+ isCocircuit_iff_minimal
+ isCocircuit_iff_minimal_compl_nonspanning
+ isCocircuit_iff_minimal_compl_nonspanning'
+ mem_fundCocircuit
+ rankPos_iff_exists_isCocircuit

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib4-dependent-issues-bot · 2025-02-10T22:20:44Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Matroid): cardinality criteria for indep/spanning sets to be bases #21512~~
By Dependent Issues (🤖). Happy coding!

…munity/mathlib4 into matroid_cocircuit

jcommelin

Thanks 🎉

bors merge

We add API for matroid cocircuits, including fundamental cocircuits and their relation to fundamental circuits. Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>

mathlib-bors · 2025-02-24T09:31:30Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)

We add API for matroid cocircuits, including fundamental cocircuits and their relation to fundamental circuits. Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>

alreadydone and others added 9 commits February 6, 2025 16:39

feat(Matroid): cardinality criteria for indep/spanning sets to be bases

42052d5

following naming convention

c9f5abe

Update Mathlib/Data/Matroid/Rank/Cardinal.lean

e8398e9

Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>

apply the other suggestion

7a4f93c

tinygolf

f46622d

Update Closure.lean

dae7cd2

initial

f4a8db6

Merge branch 'matroid_cardinal_criteria' into matroid_cocircuit

f8eebe7

wip

0aa0895

github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label Feb 10, 2025

doc

1005891

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Feb 10, 2025

apnelson1 added 5 commits February 10, 2025 17:22

Merge branch 'master' into matroid_cocircuit

38d5ced

Merge branch 'master' into matroid_cocircuit

6c0f95a

fix

d6eb152

Merge branch 'matroid_cocircuit' of https://github.com/leanprover-com…

3fb9633

…munity/mathlib4 into matroid_cocircuit

revert

27c6ca3

apnelson1 changed the title ~~feat(Data/Matroid/Circuit): Cocircuits~~ feat(Data/Matroid/Circuit): matroid cocircuits Feb 10, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 16, 2025

madvorak approved these changes Feb 17, 2025

View reviewed changes

apnelson1 added 2 commits February 17, 2025 10:58

Merge branch 'master' into matroid_cocircuit

be1455f

Merge branch 'master' into matroid_cocircuit

9cadbd6

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2025

IsCocircuit

cffe782

jcommelin reviewed Feb 24, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Feb 24, 2025

mathlib-bors Bot changed the title ~~feat(Data/Matroid/Circuit): matroid cocircuits~~ [Merged by Bors] - feat(Data/Matroid/Circuit): matroid cocircuits Feb 24, 2025

mathlib-bors Bot closed this Feb 24, 2025

mathlib-bors Bot deleted the matroid_cocircuit branch February 24, 2025 09:31

Navigation Menu

Uh oh!

[Merged by Bors] - feat(Data/Matroid/Circuit): matroid cocircuits - #21692

[Merged by Bors] - feat(Data/Matroid/Circuit): matroid cocircuits#21692
apnelson1 wants to merge 18 commits into
masterfrom
matroid_cocircuit

apnelson1 commented Feb 10, 2025 •

edited

Loading

Uh oh!

github-actions Bot commented Feb 10, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 10, 2025

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors Bot commented Feb 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Uh oh!

Conversation

apnelson1 commented Feb 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cffe782236

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 10, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Feb 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

apnelson1 commented Feb 10, 2025 •

edited

Loading

github-actions Bot commented Feb 10, 2025 •

edited

Loading