[Merged by Bors] - feat: add `[s|i]sup_toXXX` for intermediate fields and subalgebras by acmepjz · Pull Request #15088 · leanprover-community/mathlib4

acmepjz · 2024-07-23T23:32:10Z

IntermediateField.[s|i]sup_toSubfield which states that the sup, sSup and iSup for IntermediateField is the same as for Subfield.
Algebra.[s|i]sup_toSubsemiring which states that the sup, sSup and iSup for Subalgebra is the same as for Subsemiring.
Also add a missing Algebra.iInf_toSubsemiring.

discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/IntermediateField.2Esup_toSubfield

github-actions · 2024-07-23T23:32:50Z

PR summary 296dd124fe

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ adjoin_toSubfield
+ iInf_toSubsemiring
+ iSup_toSubfield
+ iSup_toSubsemiring
+ sSup_toSubfield
+ sSup_toSubsemiring
+ sup_toSubfield
+ sup_toSubsemiring
++ sSup_def
++ sup_def

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.

acmepjz · 2024-07-28T11:20:26Z

Probably Subalgebra->Subsemiring version should also be added...

Ruben-VandeVelde

Thanks!

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Mathlib/FieldTheory/Adjoin.lean

acmepjz · 2024-08-07T16:09:57Z

Sorry I'm on vacation at August; will look at it later.

acmepjz · 2024-09-03T12:04:57Z

Done.

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

b-mehta · 2024-10-04T17:12:33Z

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean


+theorem sup_def (S T : Subalgebra R A) : S ⊔ T = adjoin R (S ∪ T : Set A) := rfl
+
+theorem sSup_def (S : Set (Subalgebra R A)) : sSup S = adjoin R (⋃₀ (SetLike.coe '' S)) := rfl


The rhs here looks like it should be stated with iSup

I'm not sure about this. Since LHS is s version, I think the RHS should also be s version, i.e. sUnion. Could you give an equivalent statement in iUnion?

b-mehta · 2024-10-04T17:12:51Z

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

+open Subalgebra in
+@[simp]
+theorem sSup_toSubsemiring (S : Set (Subalgebra R A)) (hS : S.Nonempty) :
+    (sSup S).toSubsemiring = sSup (toSubsemiring '' S) := by


Similarly iSup on the right here looks nicer

I'm not sure about this. The existing result sInf_toSubsemiring uses sInf on RHS. For consistency, I think this should also use sSup instead of iSup.

b-mehta · 2024-10-04T17:13:25Z

Mathlib/FieldTheory/Adjoin.lean

    algebraMap_mem' := fun x => Subfield.subset_closure (Or.inl (Set.mem_range_self x)) }

+@[simp]
+theorem adjoin_toSubfield :


as previously

In this case it is not working, since the definition of IntermediateField extends Subalgebra but not Subfield. The @[simps] is not working at all, and @[simps!] creates IntermediateField.adjoin_carrier which is unwanted, @[simps! toSubfield] is not working either.

jcommelin

Thanks 🎉

bors merge

…15088) - `IntermediateField.[s|i]sup_toSubfield` which states that the `sup`, `sSup` and `iSup` for `IntermediateField` is the same as for `Subfield`. - `Algebra.[s|i]sup_toSubsemiring` which states that the `sup`, `sSup` and `iSup` for `Subalgebra` is the same as for `Subsemiring`. - Also add a missing `Algebra.iInf_toSubsemiring`.

mathlib-bors · 2024-10-16T05:33:37Z

Pull request successfully merged into master.

Build succeeded:

add IntermediateField.[s|i]sup_toSubfield

1b3d568

acmepjz added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jul 23, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 23, 2024

acmepjz added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 28, 2024

acmepjz mentioned this pull request Jul 28, 2024

[Merged by Bors] - feat(FieldTheory/Adjoin): add some results of extendScalars #15238

Closed

2 tasks

acmepjz added 2 commits July 29, 2024 05:16

Merge branch 'master' into acmepjz_sup_toSubfield

f374d07

add Algebra.[s|i]sup_toSubsemiring

ab8366d

acmepjz changed the title ~~feat(FieldTheory/Adjoin): add IntermediateField.[s|i]sup_toSubfield~~ feat: add [s|i]sup_toXXX for intermediate fields and subalgebras Jul 28, 2024

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 28, 2024

Ruben-VandeVelde requested changes Aug 7, 2024

View reviewed changes

acmepjz added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 7, 2024

acmepjz added 3 commits September 3, 2024 19:59

apply suggestions (1/2)

598f3d6

Merge branch 'master' into acmepjz_sup_toSubfield

4e86cb7

apply suggestions (2/2)

0a16e75

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 3, 2024

acmepjz added 4 commits September 3, 2024 20:13

revert some changes

161dc93

Merge branch 'master' into acmepjz_sup_toSubfield

a66be1c

apply suggestions

9031232

forgot

c10f78c

acmepjz requested a review from Ruben-VandeVelde September 15, 2024 20:56

b-mehta reviewed Oct 4, 2024

View reviewed changes

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 4, 2024

acmepjz added 2 commits October 5, 2024 13:13

Merge branch 'master' into acmepjz_sup_toSubfield

0021dd4

apply suggestions

296dd12

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 5, 2024

jcommelin reviewed Oct 16, 2024

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Oct 16, 2024

mathlib-bors bot changed the title ~~feat: add [s|i]sup_toXXX for intermediate fields and subalgebras~~ [Merged by Bors] - feat: add [s|i]sup_toXXX for intermediate fields and subalgebras Oct 16, 2024

mathlib-bors bot closed this Oct 16, 2024

mathlib-bors bot deleted the acmepjz_sup_toSubfield branch October 16, 2024 05:33


		theorem sup_def (S T : Subalgebra R A) : S ⊔ T = adjoin R (S ∪ T : Set A) := rfl

		theorem sSup_def (S : Set (Subalgebra R A)) : sSup S = adjoin R (⋃₀ (SetLike.coe '' S)) := rfl

Conversation

acmepjz commented Jul 23, 2024 • edited by Ruben-VandeVelde Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 296dd124fe

Import changes for modified files

Declarations diff

Uh oh!

acmepjz commented Jul 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

acmepjz commented Aug 7, 2024

Uh oh!

acmepjz commented Sep 3, 2024

Uh oh!

Uh oh!

b-mehta Oct 4, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Oct 5, 2024

Choose a reason for hiding this comment

Uh oh!

b-mehta Oct 4, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Oct 5, 2024

Choose a reason for hiding this comment

Uh oh!

b-mehta Oct 4, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Oct 5, 2024

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Oct 16, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

acmepjz commented Jul 23, 2024 •

edited by Ruben-VandeVelde

Loading

github-actions bot commented Jul 23, 2024 •

edited

Loading

acmepjz commented Jul 28, 2024 •

edited

Loading