Commit 2026-06-22 16:56 e8f2bd83

View on Github →

feat(IsGaloisGroup): add restrictHom (#38864) This PR adds the restriction map for the Galois group for domains. Given a tower of domains A ≤ B ≤ C, G a Galois group for C/A and G' a Galois group for B/A, we define:

  • restrictHom: the restriction of the G-action on C to the G'-action on B.
  • quotientMulEquiv: the isomorphism between the quotient of G by the fixing subgroup of B and the Galois group of B/A. Supporting lemmas include:
  • normal_of_isGalois: if G is a finite Galois group for L/K, H is a Galois group for L/E, and E/K is Galois, then H is a normal subgroup of G.
  • restrictHom_surjective: the restriction map is surjective.
<!-- Your PR title will become the first line of the commit message. In this box, the text above the `---` (if not empty) will be appended to the commit message, and can be used to give additional context or details. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. For details on the "pull request lifecycle" in mathlib, please see: https://leanprover-community.github.io/contribute/index.html In particular, note that most reviewers will only notice your PR if it passes the continuous integration checks. Please ask for help on https://leanprover.zulipchat.com if needed. When merging, all the commits will be squashed into a single commit listing all co-authors. Co-authors in the squash commit are gathered from two sources: First, all authors of commits to this PR branch are included. Thus, one way to add co-authors is to include at least one commit authored by each co-author among the commits in the pull request. If necessary, you may create empty commits to indicate co-authorship, using commands like so: git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor" Second, co-authors can also be listed in lines at the very bottom of the commit message (that is, directly before the `---`) using the following format: If you are moving or deleting declarations, please include these lines at the bottom of the commit message (before the `---`, and also before any "Co-authored-by" lines) using the following format: Moves: - Vector.* -> List.Vector.* - ... Deletions: - Nat.bit1_add_bit1 - ... Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] -->

Estimated changes