[Merged by Bors] - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` #15191

eric-wieser · 2022-07-08T17:22:12Z

This brings the API in line with submodule and subalgebra by removing intermediate_field.lift2 and intermediate_field.has_lift2, and replacing them with intermediate_field.restrict_scalars. This definition is strictly more general than the previous intermediate_field.lift2 definition was. A few downstream lemma statements have been generalized in the same way.

The handful of API lemmas for restrict_scalars that this adds were already missing for lift2.

intermediate_field.lift2_alg_equiv has been removed since we didn't appear to have anything similar for subalgebra or submodule, but it's possible I missed it. At any rate, it's only needed in one proof, and we can just use show or refl instead.

Note that (↑x : intermediate_field F E) is not actually a shorter spelling than x.restrict_scalars F, especially when E is more than a single character.

Finally this renames lift1 to lift now that no ambiguity remains.

…s` which replaces `lift2`

YaelDillies · 2022-07-10T13:41:02Z

src/field_theory/intermediate_field.lean

@@ -377,43 +376,45 @@ section tower

 /-- Lift an intermediate_field of an intermediate_field -/
 def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=


Let's not reproduce the vector3 naming weirdness!

Suggested change

def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=

def lift {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=

Nothing even uses this; shall I just remove it?

S.map val isn't horrible as a spelling, and we put up with it for submodules etc

I agree that we probably should get rid of it, but @kmill just introduced the subgraph analogues of it.

I'm not sure the subgraph-of-subgraph to subgraph map is a perfect analogue (I feel that combinatorial objects have somewhat different considerations from algebraic structures), but for what it's worth I've been making these sorts of shortcuts be @[reducible].

I'd vote don't remove it, and perhaps write add to the docstring to consider writing S.map val directly? That way someone trying to figure out how to do this lift can learn how to do it more easily.

Sounds like enough of a resistance that removing it is out of scope of this PR.

I'll remove the 1 suffix for now, and propose a full removal in another PR.

kmill · 2022-07-12T15:32:06Z

src/field_theory/adjoin.lean

@@ -356,10 +359,10 @@ by { conv_rhs { rw ← adjoin_simple.algebra_map_gen F α },
     rw is_integral_algebra_map_iff (algebra_map F⟮α⟯ E).injective,
     apply_instance }

-lemma adjoin_simple_adjoin_simple (β : E) : ↑F⟮α⟯⟮β⟯ = F⟮α, β⟯ :=
+lemma adjoin_simple_adjoin_simple (β : E) : F⟮α⟯⟮β⟯.restrict_scalars F = F⟮α, β⟯ :=


I wasn't sure where to leave this comment, so I'm choosing a random example.

Is F⟮α⟯⟮β⟯.restrict_scalars F now the simp normal form? I missed whether there was a simp lemma that rewrote ↑F⟮α⟯⟮β⟯ into a restrict_scalars expression.

The coercion form no longer exists, for consistency with submodule.restrict_scalars and subalgebra.restrict_scalars which also have no coercion spelling.

Vierkantor

I think this change is a good idea, especially since there is not much fallout in the dependencies. I'm not going to miss the coercion since usually you had to type-ascript it anyway.

@kmill, any further suggestions?

bors d=@kmill

src/field_theory/intermediate_field.lean

Vierkantor · 2022-07-13T09:42:04Z

src/field_theory/galois.lean

+  [hFE : finite_dimensional F E]
+  [sp : p.is_splitting_field F E] (hp : p.separable)
+  (K : Type*) [field K] [algebra F K] [algebra K E]
+  [is_scalar_tower F K E] [finite_dimensional F K]


This should follow from finite_dimensional F E + is_scalar_tower F K E (compare intermediate_field.finite_dimensional_left), but library_search isn't finding it at the moment...

Suggested change

[is_scalar_tower F K E] [finite_dimensional F K]

[is_scalar_tower F K E]

Inferring [finite_dimensional F K] from finite_dimensional F E + is_scalar_tower F K E isn't allowed because lean has no way to find E.

Of course, the instance you're thinking of is found automatically when K is an intermediate_field

Yes, but it can still be a theorem that we apply here. It turns out we have the other half: finite_dimensional.right, and basically the same should work for the left part.

The instance is needed in the theorem statement though in order to provide a fintype instance. This gets messy quite quickly; should we just take the fintype argument directly (since it carries data anyway?)

Here's a proof:

theorem finite_dimensional.left (F K E : Type*) [field F] [field K] [field E] [algebra F K] [algebra K E] [algebra F E] [is_scalar_tower F K E] [finite_dimensional F E] : finite_dimensional F K := finite_dimensional.of_injective (is_scalar_tower.to_alg_hom F K E).to_linear_map (ring_hom.injective _)

The instance is needed in the theorem statement though in order to provide a fintype instance. This gets messy quite quickly; should we just take the fintype argument directly (since it carries data anyway?)

That's a good idea actually, there are in fact already non-defeq fintype instances on alg_hom.

Arguably none of this matters anyway; this is an auxiliary lemma

I've made the change anyway, it was straightforward.

bors · 2022-07-13T09:46:52Z

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

This result came up in the discussion of #15191, where I couldn't find it. (In the end we didn't up needing it.) I saw we already had finiteness of `L / K` (in fact, for any vector space instead of the field `L`) as `finite_dimensional.right`, so I made the `left` version too. Also use this to provide an instance where `K` is an intermediate field.

src/algebra/algebra/tower.lean

bors · 2022-07-13T15:18:28Z

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

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

eric-wieser · 2022-07-13T15:20:47Z

bors merge

…s` which replaces `lift2` (#15191) This brings the API in line with `submodule` and `subalgebra` by removing `intermediate_field.lift2` and `intermediate_field.has_lift2`, and replacing them with `intermediate_field.restrict_scalars`. This definition is strictly more general than the previous `intermediate_field.lift2` definition was. A few downstream lemma statements have been generalized in the same way. The handful of API lemmas for `restrict_scalars` that this adds were already missing for `lift2`. `intermediate_field.lift2_alg_equiv` has been removed since we didn't appear to have anything similar for `subalgebra` or `submodule`, but it's possible I missed it. At any rate, it's only needed in one proof, and we can just use `show` or `refl` instead. Note that `(↑x : intermediate_field F E)` is not actually a shorter spelling than `x.restrict_scalars F`, especially when `E` is more than a single character. Finally this renames `lift1` to `lift` now that no ambiguity remains.

bors · 2022-07-13T18:30:14Z

Pull request successfully merged into master.

Build succeeded:

…5303) This result came up in the discussion of #15191, where I couldn't find it. (In the end we didn't up needing it.) I saw we already had finiteness of `L / K` (in fact, for any vector space instead of the field `L`) as `finite_dimensional.right`, so I made the `left` version too. Also use this to provide an instance where `K` is an intermediate field. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

…s` which replaces `lift2` (#15191) This brings the API in line with `submodule` and `subalgebra` by removing `intermediate_field.lift2` and `intermediate_field.has_lift2`, and replacing them with `intermediate_field.restrict_scalars`. This definition is strictly more general than the previous `intermediate_field.lift2` definition was. A few downstream lemma statements have been generalized in the same way. The handful of API lemmas for `restrict_scalars` that this adds were already missing for `lift2`. `intermediate_field.lift2_alg_equiv` has been removed since we didn't appear to have anything similar for `subalgebra` or `submodule`, but it's possible I missed it. At any rate, it's only needed in one proof, and we can just use `show` or `refl` instead. Note that `(↑x : intermediate_field F E)` is not actually a shorter spelling than `x.restrict_scalars F`, especially when `E` is more than a single character. Finally this renames `lift1` to `lift` now that no ambiguity remains.

…5303) This result came up in the discussion of #15191, where I couldn't find it. (In the end we didn't up needing it.) I saw we already had finiteness of `L / K` (in fact, for any vector space instead of the field `L`) as `finite_dimensional.right`, so I made the `left` version too. Also use this to provide an instance where `K` is an intermediate field. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

refactor(field_theory/intermediate_field): introduce `restrict_scalar…

2d5ef4d

…s` which replaces `lift2`

eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 8, 2022

eric-wieser mentioned this pull request Jul 8, 2022

[Merged by Bors] - feat(field_theory/intermediate_field): dsimp lemma #15188

Closed

1 task

add to module docstring

502a6ab

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 8, 2022

YaelDillies reviewed Jul 10, 2022

View reviewed changes

Remove unnecessary numeric suffix

9df0d19

eric-wieser requested a review from kmill July 12, 2022 08:50

kmill reviewed Jul 12, 2022

View reviewed changes

Vierkantor self-requested a review July 13, 2022 07:33

Vierkantor approved these changes Jul 13, 2022

View reviewed changes

leanprover-community-bot-assistant 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 13, 2022

eric-wieser added 2 commits July 13, 2022 10:46

clearer docstrings

3844c46

tidy fintype arguments

8242fb5

Vierkantor mentioned this pull request Jul 13, 2022

[Merged by Bors] - feat(field_theory/tower): if L / K / F is finite, so is K / F #15303

Closed

kmill reviewed Jul 13, 2022

View reviewed changes

src/algebra/algebra/tower.lean Outdated Show resolved Hide resolved

Update src/algebra/algebra/tower.lean

52826b6

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 13, 2022

bors bot changed the title ~~refactor(field_theory/intermediate_field): introduce restrict_scalars which replaces lift2~~ [Merged by Bors] - refactor(field_theory/intermediate_field): introduce restrict_scalars which replaces lift2 Jul 13, 2022

bors bot closed this Jul 13, 2022

bors bot deleted the eric-wieser/remove-lift2 branch July 13, 2022 18:30

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` #15191

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` #15191

eric-wieser commented Jul 8, 2022 •

edited

Loading

YaelDillies Jul 10, 2022

eric-wieser Jul 10, 2022

eric-wieser Jul 10, 2022

YaelDillies Jul 10, 2022

kmill Jul 10, 2022

eric-wieser Jul 10, 2022

kmill Jul 12, 2022

eric-wieser Jul 12, 2022 •

edited

Loading

Vierkantor left a comment

Vierkantor Jul 13, 2022

eric-wieser Jul 13, 2022

eric-wieser Jul 13, 2022

Vierkantor Jul 13, 2022

eric-wieser Jul 13, 2022

Vierkantor Jul 13, 2022

Vierkantor Jul 13, 2022

eric-wieser Jul 13, 2022

eric-wieser Jul 13, 2022

bors bot commented Jul 13, 2022

bors bot commented Jul 13, 2022

eric-wieser commented Jul 13, 2022

bors bot commented Jul 13, 2022

		@@ -377,43 +376,45 @@ section tower

		/-- Lift an intermediate_field of an intermediate_field -/
		def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=

	def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=
	def lift {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=

	[is_scalar_tower F K E] [finite_dimensional F K]
	[is_scalar_tower F K E]

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce restrict_scalars which replaces lift2 #15191

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce restrict_scalars which replaces lift2 #15191

Conversation

eric-wieser commented Jul 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Jul 12, 2022 • edited Loading

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bors bot commented Jul 13, 2022

bors bot commented Jul 13, 2022

eric-wieser commented Jul 13, 2022

bors bot commented Jul 13, 2022

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` #15191

[Merged by Bors] - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` #15191

eric-wieser commented Jul 8, 2022 •

edited

Loading

eric-wieser Jul 12, 2022 •

edited

Loading