liftHom or LiftHom?

Stream: mathlib4

[Lars Ericson]

Which is better, LiftHom:

CategoryTheory/Bicategory/CoherenceTactic.lean:class LiftHom {a b : B} (f : a ⟶ b) where
CategoryTheory/Bicategory/CoherenceTactic.lean:class LiftHom₂ {f g : a ⟶ b} [LiftHom f] [LiftHom g] (η : f ⟶ g) where
Tactic/CategoryTheory/Coherence.lean:class LiftHom {X Y : C} [LiftObj X] [LiftObj Y] (f : X ⟶ Y) where

or liftHom:

RingTheory/AdjoinRoot.lean:def liftHom (x : S) (hfx : aeval x f = 0) : AdjoinRoot f →ₐ[R] S :=
CategoryTheory/Bicategory/Free.lean:def liftHom : ∀ {a b : FreeBicategory B}, (a ⟶ b) → (F.obj a ⟶ F.obj b)
Algebra/QuaternionBasis.lean:def liftHom : ℍ[R,c₁,c₂] →ₐ[R] A :=

[Kyle Miller]

They're both following the naming convention. The first one is LiftHom because it's a structure/class, and the second is liftHom because it's just a definition whose value is not a type.

[Lars Ericson]

Thank you @Kyle Miller . I was having a look at CoherenceTactic.lean.

It has some capitalization issues in particular .Hom needs to be .hom in lines like

instance liftHom₂LeftUnitorHom (f : a ⟶ b) [LiftHom f] : LiftHom₂ (λ_ f).Hom
    where lift := (λ_ (LiftHom.lift f)).Hom

which doesn't typecheck but

instance liftHom₂LeftUnitorHom (f : a ⟶ b) [LiftHom f] : LiftHom₂ (λ_ f).hom
    where lift := (λ_ (LiftHom.lift f)).hom

does.

Here is an example with a mixed port of hom and Hom:

class BicategoricalCoherence (f g : a ⟶ b) [LiftHom f] [LiftHom g] where
  Hom : f ⟶ g
  [IsIso : IsIso hom]

this doesn't typecheck but changing the first Hom to hom works:

class BicategoricalCoherence (f g : a ⟶ b) [LiftHom f] [LiftHom g] where
  hom : f ⟶ g
  [IsIso : IsIso hom]

This doesn't work:

attribute [instance] bicategorical_coherence.is_iso

but this does:

attribute [instance] BicategoricalCoherence.IsIso

I'm experiencing a mix of issues on this one:

@[simps]
instance whiskerLeft (f : a ⟶ b) (g h : b ⟶ c) [LiftHom f] [LiftHom g] [LiftHom h]
    [BicategoricalCoherence g h] : BicategoricalCoherence (f ≫ g) (f ≫ h) :=
  ⟨f ◁ BicategoricalCoherence.hom g h⟩

It prefers @[simps!] to @[simps]. The bigger problem is that it doesn't accept the g h following BicategoricalCoherence.hom , which has type

CategoryTheory.Bicategory.BicategoricalCoherence.hom.{w, v, u} {B : Type u} [inst✝ : Bicategory B] {a b : B}
  {f g : a ⟶ b} [inst✝¹ : LiftHom f] [inst✝² : LiftHom g] [self : BicategoricalCoherence f g] : f ⟶ g

If I simply omit the g h in BicategoricalCoherence.hom g h, this typechecks:

@[simps!]
instance whiskerLeft (f : a ⟶ b) (g h : b ⟶ c) [LiftHom f] [LiftHom g] [LiftHom h]
    [BicategoricalCoherence g h] : BicategoricalCoherence (f ≫ g) (f ≫ h) :=
  ⟨f ◁ BicategoricalCoherence.hom ⟩

Also on this one which doesn't typecheck:

instance tensorRight (f : a ⟶ b) (g : b ⟶ b) [LiftHom f] [LiftHom g]
    [BicategoricalCoherence (𝟙 b) g] : BicategoricalCoherence f (f ≫ g) :=
  ⟨(ρ_ f).inv ≫ f ◁ BicategoricalCoherence.hom (𝟙 b) g⟩

omitting the arguments (𝟙 b) g to BicategoricalCoherence.hom works

instance tensorRight (f : a ⟶ b) (g : b ⟶ b) [LiftHom f] [LiftHom g]
    [BicategoricalCoherence (𝟙 b) g] : BicategoricalCoherence f (f ≫ g) :=
  ⟨(ρ_ f).inv ≫ f ◁ BicategoricalCoherence.hom ⟩

but feels a little worrisome to me to simply elide the more complex argument pattern.

[Lars Ericson]

I'm also having a problem with infix notation for example assuming

scoped[Bicategory] infixr:80 " ⊗≫ " => CategoryTheory.Bicategory.bicategoricalComp

then this fails:

example {f' : a ⟶ d} {f : a ⟶ b} {g : b ⟶ c} {h : c ⟶ d} {h' : a ⟶ d} (η : f' ⟶ f ≫ g ≫ h)
    (θ : (f ≫ g) ≫ h ⟶ h') : f' ⟶ h' :=
   η ⊗≫ θ

but this works:

example {f' : a ⟶ d} {f : a ⟶ b} {g : b ⟶ c} {h : c ⟶ d} {h' : a ⟶ d} (η : f' ⟶ f ≫ g ≫ h)
    (θ : (f ≫ g) ≫ h ⟶ h') : f' ⟶ h' :=
   CategoryTheory.Bicategory.bicategoricalComp η θ

[Damiano Testa]

The scoped issue may be that you need to explicitly mention the full namespace, not just the last part. In your case, possibly

scoped[CategoryTheory.Bicategory] infixr:80 " ⊗≫ " => CategoryTheory.Bicategory.bicategoricalComp

will work?

[Damiano Testa]

Regarding capitalizations, that is the first part of "trivial fixes" that every ported file has.

[Adam Topaz]

@Lars Ericson the hom vs Hom thing you just mentioned is still fully expected with the naming convention.

[Adam Topaz]

Here hom refers to a morphism projection which part of docs4#CategoryTheory.Iso

[Lars Ericson]

@Damiano Testathanks adding CategoryTheory. to the name in scoped makes subsequent uses work.

[Lars Ericson]

I am down to the last few lines in the file having to do with tactics. From the original , this:

meta def bicategorical_coherence : tactic unit :=
focus1 $
do
  o ← get_options, set_options $ o.set_nat `class.instance_max_depth 128,
  try `[dsimp],
  `(%%lhs = %%rhs) ← target,
  to_expr  ``((free_bicategory.lift (prefunctor.id _)).map₂ (lift_hom₂.lift %%lhs) =
    (free_bicategory.lift (prefunctor.id _)).map₂ (lift_hom₂.lift %%rhs))
    >>= tactic.change,
  congr

gets translated as

/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/
/- ./././Mathport/Syntax/Translate/Expr.lean:330:4: warning: unsupported (TODO): `[tacs] -/
-- failed to format: unknown constant 'term.pseudo.antiquot'
/-- Coherence tactic for bicategories. -/ unsafe
  def
    bicategorical_coherence
    : tactic Unit
    :=
      focus1
        do
          let o ← get_options
            set_options <| o `class.instance_max_depth 128
            try sorry
            let q( $ ( lhs ) = $ ( rhs ) ) ← target
            to_expr
                `
                  `(
                    ( FreeBicategory.lift ( Prefunctor.id _ ) ) . zipWith
                        ( LiftHom₂.lift $ ( lhs ) )
                      =
                      ( FreeBicategory.lift ( Prefunctor.id _ ) ) . zipWith
                        ( LiftHom₂.lift $ ( rhs ) )
                    )
              >>=
              tactic.change
            congr

and this

meta def whisker_simps : tactic unit :=
`[simp only [
    category_theory.category.assoc,
    category_theory.bicategory.comp_whisker_left,
    category_theory.bicategory.id_whisker_left,
    category_theory.bicategory.whisker_right_comp,
    category_theory.bicategory.whisker_right_id,
    category_theory.bicategory.whisker_left_comp,
    category_theory.bicategory.whisker_left_id,
    category_theory.bicategory.comp_whisker_right,
    category_theory.bicategory.id_whisker_right,
    category_theory.bicategory.whisker_assoc]]

gets translated as

/- ./././Mathport/Syntax/Translate/Expr.lean:330:4: warning: unsupported (TODO): `[tacs] -/
/-- Simp lemmas for rewriting a 2-morphism into a normal form. -/
unsafe def whisker_simps : tactic Unit :=
  sorry

Both are getting autoported to sorry and the second one which looks easier to solve is also the most sorry.

It is hard to find uses in Lean 3 mathlib of '[simp only. Here is an original use on line 164:

meta def tactic.interactive.push_neg : parse location → tactic unit
| (loc.ns loc_l) :=
  loc_l.mmap'
    (λ l, match l with
          | some h := do push_neg_at_hyp h,
                          try $ interactive.simp_core { eta := ff } failed tt
                                 [simp_arg_type.expr ``(push_neg.not_eq)] []
                                 (interactive.loc.ns [some h])
          | none   := do push_neg_at_goal,
                          try `[simp only [push_neg.not_eq] { eta := ff }]
          end)
| loc.wildcard := do
    push_neg_at_goal,
    local_context >>= mmap' (λ h, push_neg_at_hyp (local_pp_name h)) ,
    try `[simp only [push_neg.not_eq] at * { eta := ff }]

This has a complex rewrite in the ported version

syntax (name := pushNegConv) "push_neg" : conv

@[tactic pushNegConv] def elabPushNegConv : Tactic := fun _ ↦ withMainContext do
  Conv.applySimpResult (← pushNegCore (← instantiateMVars (← Conv.getLhs)))

macro (name := pushNeg) tk:"#push_neg " e:term : command => `(command| #conv%$tk push_neg => $e)

The tactic rewrites look very expert level. I won't attempt. I did manage to get the first 250 lines to typecheck though. As recommended by @Yaël Dillies I would like to submit a PR with help-wanted tag. While I can run the start_port.sh without credentials, to go the other way it is asking me for some. I did

git add Mathlib/CategoryTheory/Bicategory/CoherenceTactic.lean
git commit -m "First 250 lines now typecheck, rest is tactics"

I have a github account so I supplied those credentials. I got this error on the git push:

$ git push
fatal: not a git repository (or any of the parent directories): .git

Maybe I missed a step of cloning Mathlib4 to my personal GitHub before running the start_port.sh. Do you have a step-by-step for new users on how to get set up, up to and including where and how to enter the pull request with the tags?

[Lars Ericson]

For now I'll put it here

CoherenceTactic.lean

[Scott Morrison]

Were you in the same directory when you ran the git commit and the git push? It seems strange that the first could succeed while the second can't find a .git directory...

[Lars Ericson]

@Scott Morrison I can do a local commit but there is no place to push it to. I don't think that start_port.sh is permissioning me to upload to the repository that it pulls from. It is just cloning a public repository and bringing it down to my PC. That doesn't require any permissions. I would need an access token to the public repository branch to do a git push. Here is what I see:

~/mathlib4$ git status
On branch port/CategoryTheory.Bicategory.CoherenceTactic
nothing to commit, working tree clean

~/mathlib4$ git push
fatal: The current branch port/CategoryTheory.Bicategory.CoherenceTactic has no upstream branch.
To push the current branch and set the remote as upstream, use

    git push --set-upstream origin port/CategoryTheory.Bicategory.CoherenceTactic

~/mathlib4$ git push --set-upstream origin port/CategoryTheory.Bicategory.CoherenceTactic
Username for 'https://github.com': catskills
Password for 'https://catskills@github.com':
remote: Permission to leanprover-community/mathlib4.git denied to catskillsresearch.
fatal: unable to access 'https://github.com/leanprover-community/mathlib4.git/': The requested URL returned error: 403

So to push I need permission to push to leanprover-community/mathlib4.git, for which I would need a login and an API access token. It seems more likely that I would push to a github that I own and then do a pull request referencing that github. However, to do that, I would also need to have created a clone in my remote github of the mathlib4 repo, which start_port.sh didn't do.

I need more clarification on the setup to do a PR as recommended.

[Lars Ericson]

I found this guidance :

We are currently overwhelmed. We respectfully request that you hold off on submitting Pull Requests and creating Request for Comments (RFCs) at this time. Our team is actively seeking funding to expand the Lean development team and improve our capacity to review and integrate contributions. We appreciate your understanding and look forward to being able to accept contributions in the near future. In the meantime, the process described in the following sections is temporarily suspended.

So, I can clone mathlib4, upload my draft of CoherenceTactic, and submit a PR, but per above the PR would be unwelcome. It seems like it would be good to get that one done, though, because it would unblock 43 other files. To eliminate the paperwork, my file is above. There are a few other short leaf nodes I can work on. If I get them to typecheck an alternate path is to upload them to new members thread with a comment.

[Lars Ericson]

In particular order.category.HeytAlg seems short and unattended, and has a bunch of unattended dependencies.

[Oisin McGuinness]

Hi Lars, I believe the quoted guidance refers to issues and requests arising for Lean4 itself, which are handled by a small group of Lean developers, and do not apply for mathlib4 porting or PRs for mathlib4 itself.

[Lars Ericson]

Thanks @Oisin McGuinness! Can you summarize the steps to take after editing a file pulled down with scripts/start_port.sh to upload the file and do a PR?

[Oisin McGuinness]

I believe current information about porting is here: https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki
I have not yet attempted a port :-)

[Lars Ericson]

Oisin, my thinking is that step Porting wiki > Porting status > Porting procedure > High level > 4. "Publish the new branch" requires trusted status, an account and an API key on the mathlib4 repo. That is the part of the process I am confused about.

That said I encourage you to find something to port as long as porting is welcome. The port status is here. I have been shopping in the middle section of "Unported files", sorting by lines of code on the left and looking for shortest files with no dependencies. Sometimes I find a file with no dependencies which looks portable but is not because of a directory reorganization for example Module to ModuleCat which can leave an apparently portable file which is actually already elsewhere. I found that most files have the root nodes of their dependency graph blocked by a yellow file which is claimed but not completely ported. So there are actually not that many with no dependencies which are unclaimed, like the bunch of files around order.category.HeytAlg.

My original object of interest was weierstrass. That one has been steadily progressing but the leaf nodes are always yellow:

Screenshot-from-2023-05-28-22-54-00.png

[Lars Ericson]

(deleted)

[Johan Commelin]

I personally find it quite tiring that you turn almost every discussion into something about money / funding crisis / etc...

[Ruben Van de Velde]

Lars, if you want to help with porting mathlib, you will need to ask here for permission to push to mathlib 4. There's no point in starting otherwise.

[Damiano Testa]

And if you want to do some fundraising, I think that the community here would very much welcome a grant!

However, I think that fundraising would have to take place outside of this community.

Everyone here is already volunterring what time they can.

[Lars Ericson]

@Ruben Van de Velde, I would like permission to do a PR help-wanted for the attached file for Mathlib/CategoryTheory/Bicategory/CoherenceTactic.lean. It cleans up the file up to line 252, where there is a tactic section that needs expert level porting.
CoherenceTactic.lean

[Johan Commelin]

That file has already been ported last week.

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/4357

[Lars Ericson]

@Johan Commelin given that Mathlib/CategoryTheory/Bicategory/CoherenceTactic.lean was ported, what is the new home of the contents? It is not here:

https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory/Bicategory

but it was here:

https://github.com/leanprover-community/mathlib/blob/13b0d72fd8533ba459ac66e9a885e35ffabb32b2/src/category_theory/bicategory/coherence_tactic.lean

and it is also still here:

https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/CategoryTheory/Bicategory/CoherenceTactic.lean

and it is still in the Unported files list here:

https://leanprover-community.github.io/mathlib-port-status/file/category_theory/bicategory/coherence_tactic

[Johan Commelin]

Do you have experience with writing tactics? Otherwise this doesn't seem like a good file to worry about.

[Johan Commelin]

You can answer your question about the new location by looking at the PR that I linked to above.

[Lars Ericson]

@Johan Commelin reading the PR it seems that CategoryTheory.Bicategory.CoherenceTactic got merged into Tactic.CategoryTheory.Coherence. That has a FreeMonoidalCategory with a LiftHom class. Does FreeMonoidalCategory replace Bicategory? Or the is Bicategory LiftHom class gone? I see this note in the ported file:

-- Porting note: restore when ported
-- import Mathlib.CategoryTheory.Bicategory.CoherenceTactic

The PR notes start with

It does not include a port of the coherence tactic for bicategories, but this is not actually used in mathlib yet.

In any event if CoherenceTactic was merged and ported, it would be helpful to exclude this page

https://leanprover-community.github.io/mathlib-port-status/file/category_theory/bicategory/coherence_tactic

from the Mathlib porting status.