test(library/theories/group_theory): test auto-include in the group theory library
This commit is contained in:
parent
ce622e9179
commit
49eae56db4
4 changed files with 31 additions and 69 deletions
|
@ -129,8 +129,7 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [add_comm_monoid A] : comm_
|
|||
⦄
|
||||
|
||||
section add_comm_monoid
|
||||
variables [s : add_comm_monoid A]
|
||||
include s
|
||||
variables [add_comm_monoid A]
|
||||
|
||||
theorem add_comm_three (a b c : A) : a + b + c = c + b + a :=
|
||||
by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc]
|
||||
|
@ -147,9 +146,7 @@ structure group [class] (A : Type) extends monoid A, has_inv A :=
|
|||
-- Note: with more work, we could derive the axiom one_mul
|
||||
|
||||
section group
|
||||
|
||||
variable [s : group A]
|
||||
include s
|
||||
variable [group A]
|
||||
|
||||
theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
|
||||
|
||||
|
@ -306,19 +303,18 @@ section group
|
|||
x*y ∘c c = x ∘c y ∘c c : conj_compose
|
||||
... = x ∘c b : Py
|
||||
... = a : Px)
|
||||
|
||||
definition group.to_left_cancel_semigroup [trans_instance] [reducible] :
|
||||
left_cancel_semigroup A :=
|
||||
⦃ left_cancel_semigroup, s,
|
||||
mul_left_cancel := @mul_left_cancel A s ⦄
|
||||
|
||||
definition group.to_right_cancel_semigroup [trans_instance] [reducible] :
|
||||
right_cancel_semigroup A :=
|
||||
⦃ right_cancel_semigroup, s,
|
||||
mul_right_cancel := @mul_right_cancel A s ⦄
|
||||
|
||||
end group
|
||||
|
||||
definition group.to_left_cancel_semigroup [trans_instance] [reducible] [s : group A] :
|
||||
left_cancel_semigroup A :=
|
||||
⦃ left_cancel_semigroup, s,
|
||||
mul_left_cancel := @mul_left_cancel A s ⦄
|
||||
|
||||
definition group.to_right_cancel_semigroup [trans_instance] [reducible] [s : group A] :
|
||||
right_cancel_semigroup A :=
|
||||
⦃ right_cancel_semigroup, s,
|
||||
mul_right_cancel := @mul_right_cancel A s ⦄
|
||||
|
||||
structure comm_group [class] (A : Type) extends group A, comm_monoid A
|
||||
|
||||
/- additive group -/
|
||||
|
@ -332,7 +328,6 @@ definition add_group.to_group {A : Type} [add_group A] : group A :=
|
|||
|
||||
|
||||
section add_group
|
||||
|
||||
variables [s : add_group A]
|
||||
include s
|
||||
|
||||
|
|
|
@ -15,13 +15,12 @@ private lemma and_left_true {a b : Prop} (Pa : a) : a ∧ b ↔ b :=
|
|||
by rewrite [iff_true_intro Pa, true_and]
|
||||
|
||||
section def
|
||||
variables {G S : Type} [ambientG : group G] [finS : fintype S] [deceqS : decidable_eq S]
|
||||
include ambientG finS
|
||||
variables {G S : Type} [group G] [fintype S]
|
||||
|
||||
definition is_fixed_point (hom : G → perm S) (H : finset G) (a : S) : Prop :=
|
||||
∀ h, h ∈ H → hom h a = a
|
||||
|
||||
include deceqS
|
||||
variables [decidable_eq S]
|
||||
|
||||
definition orbit (hom : G → perm S) (H : finset G) (a : S) : finset S :=
|
||||
image (move_by a) (image hom H)
|
||||
|
@ -29,8 +28,7 @@ definition orbit (hom : G → perm S) (H : finset G) (a : S) : finset S :=
|
|||
definition fixed_points [reducible] (hom : G → perm S) (H : finset G) : finset S :=
|
||||
{a ∈ univ | orbit hom H a = singleton a}
|
||||
|
||||
variable [deceqG : decidable_eq G]
|
||||
include deceqG -- required by {x ∈ H |p x} filtering
|
||||
variable [decidable_eq G] -- required by {x ∈ H |p x} filtering
|
||||
|
||||
definition moverset (hom : G → perm S) (H : finset G) (a b : S) : finset G :=
|
||||
{f ∈ H | hom f a = b}
|
||||
|
@ -42,13 +40,7 @@ end def
|
|||
|
||||
section orbit_stabilizer
|
||||
|
||||
variables {G S : Type}
|
||||
variable [ambientG : group G]
|
||||
include ambientG
|
||||
variable [finS : fintype S]
|
||||
include finS
|
||||
variable [deceqS : decidable_eq S]
|
||||
include deceqS
|
||||
variables {G S : Type} [group G] [fintype S] [decidable_eq S]
|
||||
|
||||
section
|
||||
|
||||
|
@ -108,8 +100,7 @@ by rewrite [fixed_points_of_one]
|
|||
|
||||
end
|
||||
|
||||
variable [deceqG : decidable_eq G]
|
||||
include deceqG
|
||||
variable [decidable_eq G]
|
||||
|
||||
-- these are already specified by stab hom H a
|
||||
variables {hom : G → perm S} {H : finset G} {a : S}
|
||||
|
@ -152,8 +143,7 @@ lemma moverset_inj_on_orbit : set.inj_on (moverset hom H a) (ts (orbit hom H a))
|
|||
apply of_mem_sep Ph1b1
|
||||
end
|
||||
|
||||
variable [subgH : is_finsubg H]
|
||||
include subgH
|
||||
variable [is_finsubg H]
|
||||
|
||||
lemma subg_stab_of_move {h g : G} :
|
||||
h ∈ H → g ∈ moverset hom H a (hom h a) → h⁻¹*g ∈ stab hom H a :=
|
||||
|
@ -244,7 +234,7 @@ lemma subg_moversets_of_orbit_eq_stab_lcosets :
|
|||
existsi h, subst Pb₂, assumption
|
||||
end)
|
||||
(assume Pr, obtain h Ph₁ Ph₂, from exists_of_mem_image Pr,
|
||||
obtain b Pb, from @subg_lcoset_of_stab_is_moverset_of_orbit G S ambientG finS deceqS deceqG hom H a Hom subgH h Ph₁, begin
|
||||
obtain b Pb, from @subg_lcoset_of_stab_is_moverset_of_orbit G S _ _ _ _ hom H a Hom _ h Ph₁, begin
|
||||
rewrite [mem_image_eq],
|
||||
existsi b, subst Ph₂, assumption
|
||||
end))
|
||||
|
@ -260,9 +250,7 @@ end orbit_stabilizer
|
|||
|
||||
section orbit_partition
|
||||
|
||||
variables {G S : Type} [ambientG : group G] [finS : fintype S]
|
||||
variables [deceqS : decidable_eq S]
|
||||
include ambientG finS deceqS
|
||||
variables {G S : Type} [group G] [fintype S] [decidable_eq S]
|
||||
variables {hom : G → perm S} [Hom : is_hom_class hom] {H : finset G} [subgH : is_finsubg H]
|
||||
include Hom subgH
|
||||
|
||||
|
@ -377,17 +365,12 @@ calc card S = Sum (orbits hom H) finset.card
|
|||
end orbit_partition
|
||||
|
||||
section cayley
|
||||
variables {G : Type}
|
||||
variable [ambientG : group G]
|
||||
include ambientG
|
||||
variable [finG : fintype G]
|
||||
include finG
|
||||
variables {G : Type} [group G] [fintype G]
|
||||
|
||||
definition action_by_lmul : G → perm G :=
|
||||
take g, perm.mk (lmul_by g) (lmul_inj g)
|
||||
|
||||
variable [deceqG : decidable_eq G]
|
||||
include deceqG
|
||||
variable [decidable_eq G]
|
||||
|
||||
lemma action_by_lmul_hom : homomorphic (@action_by_lmul G _ _) :=
|
||||
take g₁ (g₂ : G), eq.symm (calc
|
||||
|
@ -411,8 +394,7 @@ end cayley
|
|||
section lcosets
|
||||
open fintype subtype
|
||||
|
||||
variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
|
||||
include ambientG deceqG finG
|
||||
variables {G : Type} [group G] [fintype G] [decidable_eq G]
|
||||
|
||||
variables H : finset G
|
||||
|
||||
|
|
|
@ -18,9 +18,7 @@ open ops
|
|||
|
||||
section subg
|
||||
-- we should be able to prove properties using finsets directly
|
||||
variable {G : Type}
|
||||
variable [ambientG : group G]
|
||||
include ambientG
|
||||
variables {G : Type} [group G]
|
||||
|
||||
definition finset_mul_closed_on [reducible] (H : finset G) : Prop :=
|
||||
∀ x y : G, x ∈ H → y ∈ H → x * y ∈ H
|
||||
|
@ -47,8 +45,7 @@ lemma finsubg_mul_closed (H : finset G) [h : is_finsubg H] {x y : G} : x ∈ H
|
|||
lemma finsubg_has_inv (H : finset G) [h : is_finsubg H] {a : G} : a ∈ H → a⁻¹ ∈ H :=
|
||||
@is_finsubg.has_inv G _ H h a
|
||||
|
||||
variable [deceqG : decidable_eq G]
|
||||
include deceqG
|
||||
variable [decidable_eq G]
|
||||
|
||||
definition finsubg_to_subg [instance] {H : finset G} [h : is_finsubg H]
|
||||
: is_subgroup (ts H) :=
|
||||
|
@ -72,11 +69,7 @@ section fin_lcoset
|
|||
|
||||
open set
|
||||
|
||||
variable {A : Type}
|
||||
variable [deceq : decidable_eq A]
|
||||
include deceq
|
||||
variable [s : group A]
|
||||
include s
|
||||
variables {A : Type} [decidable_eq A] [group A]
|
||||
|
||||
definition fin_lcoset (H : finset A) (a : A) := finset.image (lmul_by a) H
|
||||
|
||||
|
@ -195,8 +188,7 @@ end
|
|||
section lcoset_fintype
|
||||
open fintype list subtype
|
||||
|
||||
variables {A : Type} [ambientA : group A] [finA : fintype A] [deceqA : decidable_eq A]
|
||||
include ambientA deceqA finA
|
||||
variables {A : Type} [group A] [fintype A] [decidable_eq A]
|
||||
|
||||
variables G H : finset A
|
||||
|
||||
|
|
|
@ -12,12 +12,8 @@ namespace group_theory
|
|||
open fintype
|
||||
|
||||
section perm
|
||||
variable {A : Type}
|
||||
variable [finA : fintype A]
|
||||
include finA
|
||||
variable [deceqA : decidable_eq A]
|
||||
include deceqA
|
||||
variable {f : A → A}
|
||||
variables {A : Type} [fintype A] [decidable_eq A]
|
||||
variable {f : A → A}
|
||||
|
||||
lemma perm_surj : injective f → surjective f :=
|
||||
surj_of_inj_eq_card (eq.refl (card A))
|
||||
|
@ -44,9 +40,7 @@ structure perm (A : Type) [h : fintype A] : Type :=
|
|||
local attribute perm.f [coercion]
|
||||
|
||||
section perm
|
||||
variable {A : Type}
|
||||
variable [finA : fintype A]
|
||||
include finA
|
||||
variables {A : Type} [fintype A]
|
||||
|
||||
lemma eq_of_feq : ∀ {p₁ p₂ : perm A}, (perm.f p₁) = p₂ → p₁ = p₂
|
||||
| (perm.mk f₁ P₁) (perm.mk f₂ P₂) := assume (feq : f₁ = f₂), by congruence; assumption
|
||||
|
@ -62,8 +56,7 @@ lemma perm.f_mk {f : A → A} {Pinj : injective f} : perm.f (perm.mk f Pinj) = f
|
|||
|
||||
definition move_by [reducible] (a : A) (f : perm A) : A := f a
|
||||
|
||||
variable [deceqA : decidable_eq A]
|
||||
include deceqA
|
||||
variable [decidable_eq A]
|
||||
|
||||
lemma perm.has_decidable_eq [instance] : decidable_eq (perm A) :=
|
||||
take f g,
|
||||
|
|
Loading…
Reference in a new issue