Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(model_theory/basic): more substructure API, including subtype, map, and comap #7937

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(model_theory/basic): more substructure API, including subtype, map, and comap #7937

wants to merge 15 commits into from

Conversation

awainverse
Copy link
Collaborator

@awainverse awainverse commented Jun 14, 2021 •
edited by github-actions bot

Defines first_order.language.embedding.of_injective, which bundles an injective hom in an algebraic language as an embedding
Defines the induced L.Structure on an L.substructure
Defines the embedding S.subtype from S : L.substructure M into M
Defines substructure.map and substructure.comap and associated API including Galois insertions

This is mostly copied from the submonoid API.

Open in Gitpod

@awainverse awainverse added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jun 14, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jun 17, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 17, 2021
jcommelin
jcommelin reviewed Jun 22, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mostly looks good to me. Some minor comments.

src/model_theory/basic.lean Show resolved Hide resolved
src/model_theory/basic.lean Outdated Show resolved Hide resolved
src/model_theory/basic.lean Outdated Show resolved Hide resolved
src/model_theory/basic.lean Outdated
lemma map_map (g : N →[L] P) (f : M →[L] N) : (S.map f).map g = S.map (g.comp f) :=
set_like.coe_injective $ image_image _ _ _


Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There seem to be a bunch of double empty lines between the lemma declarations here. Is that intentional?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you give a motivation?

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 22, 2021
@awainverse awainverse added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 30, 2021
Vierkantor
Vierkantor approved these changes Jul 16, 2021
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the wait!

bors d+

src/model_theory/basic.lean Outdated Show resolved Hide resolved
src/model_theory/basic.lean Outdated
lemma map_map (g : N →[L] P) (f : M →[L] N) : (S.map f).map g = S.map (g.comp f) :=
set_like.coe_injective $ image_image _ _ _


Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you give a motivation?

@bors
Copy link

bors bot commented Jul 16, 2021

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 16, 2021
@jcommelin
Copy link
Member

@awainverse As far as I can see, this is mostly ready to go. Are you planning to return to this in the near future?

@awainverse
Copy link
Collaborator Author

I've just finished a long break while I've had a summer job - I'll push my changes and try to merge this once I can figure out personal access tokens.

@awainverse
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Aug 18, 2021
@awainverse
feat(model_theory/basic): more substructure API, including subtype, m…
15444e1 
…ap, and comap (#7937)

Defines `first_order.language.embedding.of_injective`, which bundles an injective hom in an algebraic language as an embedding
Defines the induced `L.Structure` on an `L.substructure`
Defines the embedding `S.subtype` from `S : L.substructure M` into `M`
Defines `substructure.map` and `substructure.comap` and associated API including Galois insertions
@bors
Copy link

bors bot commented Aug 18, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(model_theory/basic): more substructure API, including subtype, map, and comap [Merged by Bors] - feat(model_theory/basic): more substructure API, including subtype, map, and comap Aug 18, 2021
@bors bors bot closed this Aug 18, 2021
@bors bors bot deleted the sub_induced_structure branch August 18, 2021 21:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@awainverse @jcommelin @Vierkantor